Learning/Teaching Coinduction with Coq

This semester Benjamin Pierce gave a course on Advanced Coq Martial Arts based on Adam Chlipala’s CPDT book. The course was very interactive, with the students giving most of the lectures and being in charge of creating the exercises. Since I wanted to know more about coinduction I taught the coinduction lectures and learned a lot in the process. One of the results of these lectures is a new set of materials for teaching coinduction in Coq:

• An Introduction to Coinduction
• Coinductive Operational Semantics

These materials are based on Adam’s book chapter, Giménez and Castéran’s tutorial, and Xavier Leroy and Herve Grall’s development on coinductive operational semantics. I’ve tried my best to explain things better and to add good exercises.

Another result is a new Coq tactic that allows for aggressive automation of coinductive proofs. Most of the easy proofs now take the form coind using coind_principle; crush.

• Full Coq development including my coind tactic

Update 2012-12-25:

The Saarbrücken Graduate School in Computer Science

• An integrated program from BSc or MSc to PhD
• Top-notch academic and research training in computer science
• Unparalleled concentration of computer science research expertise in Europe
• International program run entirely in English
• Scholarships and other forms of financial support
• Next application deadline: 29 April 2011 uptake Winter Semester 2011/12 (October)
• More information at
  http://frweb.cs.uni-sb.de/index.php?id=7&L=0

Mobility of Young People in Europe (Questionnaire)

Young? Fond of traveling abroad to boost your education? What exactly do you expect to gain when studying abroad? Or when doing an internship abroad? Or when just doing a trip in some other country? Which advantages and disadvantages does a young person have when being mobile?

The Young European Federalists (JEF) want to study these questions and need your support. Their online questionnaire contains questions about mobility during education & training and requires approximately 10 minutes for filling in:

English Version/ German Version / French Version

Evaluation is anonymous and the results will be published after the 1st of August 2009 on the JEF website. JEF will use the results to make suggestions to politicians in order to achieve equal opportunities, to provide support and information for young people who want to travel abroad.

Typed Operational Reasoning

This semester I’m attending Derek‘s course on Typed Operational Reasoning. Description from the site:

While many theorems about type systems are provable by straightforward induction, some properties are much trickier to prove and require a clever insight into how to “strengthen the induction hypothesis”. The method of logical relations provides such an insight, and it has been applied, generalized, and extended to prove a variety of interesting properties about typed programs. These include termination, strong normalization, decidability of type checking, consistency of type equivalence, contextual equivalence of programs, effectiveness of data abstraction mechanisms, and validity of program transformations. We will introduce the idea as it originated–Tait’s method for proving termination/strong normalization for the simply-typed lambda calculus–and eventually work our way up to equational reasoning about programs in a language supporting polymorphism, existential types, recursive functions, recursive types, and mutable references. Although the logical relations method is often used in the setting of denotational semantics, we will focus on how to use it to do operational reasoning about typed programs.

A secondary goal of the course is to convey a sense of how one actually does research and makes progress in programming language theory, or at least how I do it. Although classic results are often presented in the literature without any hint of their origins, in reality there is a continual, subtle interplay between the act of proving theorems and the act of discovering what theorems one wants to prove. (This is closely related to what Lakatos calls “the method of proofs and refutations”.) I will try to convey this interplay in the presentation of a number of topics in the course.

My First Students

Last week two of the students I supervise submitted their Bachelor’s Thesis. Both theses are about automatically generating executable code from abstract specifications of security protocols, however, the focus is quite different. While Alex worked on a very powerful tool that generates interoperable protocol implementations (to be released soon), Thorsten formalized a much simpler code generator and proved it to the preserve the security of the original protocol. In the future we would like of course to have both, the extensibility, flexibility and interoperability of Alex’ tool, with the same strong security guarantees as Thorsten proves for his generated code.

• Expi2Java – An Extensible Code Generator for Security Protocols (Alex Busenius)
  Abstract: This thesis presents expi2java, an extensible code generator for security protocols. We use a variant of Spi calculus for the protocol specifications and complement it with an expressive type system that is designed to reject inconsistent protocols. This type system features subtyping and parametric polymorphism. It is able to handle the types of nested terms, specialized channels and even low-level term configurations. Expi2java is highly customizable, easily extensible and generates interoperable Java code. We show the flexibility of our approach by generating an implementation of the Transport Layer Security (TLS) protocol.
• Spi2F# – A Prototype Code Generator for Security Protocols (Thorsten Tarrach)
  Abstract: This thesis describes a new prototype tool that automatically generates a secure F# implementation of any protocol described in the Spi calculus. Type systems were previously proposed for analysing the security of both Spi calculus processes and F# implementations. The thesis investigates a formal translation from the Spi calculus to F# that is proved to preserve typability, and therefore the security properties of the original protocol are preserved.

Summer School: GLOBAN 2008

This week I was in Warsaw where I attended the “Global Computing Approach to the Analysis of Systems” (GLOBAN) Summer School. The school is was (very well) organized by University of Warsaw, in association with the MOBIUS and SENSORIA European projects. The eight distinguished lecturers did a really good job introducing us to their research: Rocco De Nicola, Andrew D. Gordon, Reiko Heckel, Martin Hofmann, Joost-Pieter Katoen, Joe Kiniry, Flemming Nielson, and Andrei Sabelfeld.

All the materials (including slides and references) are available online, and so are some of the photos. My photos from Warsaw will also be available soon.

Summer School: VTSA 2008

Last week I attended the first “Verification Technology, Systems & Applications (VTSA 2008)” summer school at the Max Planck Institute for Informatics in Saarbrücken. The talks were very interesting and all the slides are available online. Some photos from the event are also available.

The course I liked the most was given by Grégoire Sutre and was about Static Analysis, Abstract Interpretation and Abstraction Refinement.

Course: Working with Automated Reasoning Tools

In the first week of September I attended a very interesting lecture entitled “Working with Automated Reasoning Tools”, given by Christoph Benzmueller (Saarland University) and Geoff Sutcliffe (University of Miami). The two most important highlights were the LEO-II automatic higher-order theorem prover and the TPTP theorem proving infrastructure (including the comprehensive TPTP problem and solution libraries, the TPTP syntax for first-order and higher-order logic, and the hordes of automatic theorem provers and many TPTP tools that can be called from any web browser using System-on-TPTP).

All the course materials are available online.

Computer Science Research in Saarbrücken Gets More Funding

Both excellence proposals in Computer Science coming from Saarbrücken were accepted. One proposal concerns a new graduate school which will encompass all graduate education in Computer Science at Saarland University. The other is about a new “Multimodal Computing and Interaction” excellence cluster which will host 20 new research groups. Happy, happy, joy, joy

Press release in English

Buy a Mac, Get an iPod Nano

Now in Germany too