December 23, 2012
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:
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.
Read the rest of this entry »
May 13, 2011
Alex Busenius and me are pleased to announce that Expi2Java 1.6 was released two days ago. And by the way, Alex has recently finished his MSc and is looking for a job in industry. If you know anything interesting in a German or English speaking country, please let him know.
Expi2Java 1.6 was released yesterday (11.05.2011)
The highlights of this release are the new symbolic library and a mechanized formalization in Coq.
The symbolic library abstracts away cryptographic primitives as symbolic terms and networking as pi-calculus-like channels. It is designed to be sound and simple enough to simplify proving the transformation secure. Both the symbolic and concrete libraries can be used interchangeably with all provided examples.
We have formalized the transformation from Expi Calculus to a subset of Java performed by Expi2Java using the Coq proof assistant and proved the symbolic library and the produced Java code to be well-typed. The formalization and all proofs can be found on the project homepage.
The full list of changes: Read the rest of this entry »
November 11, 2010
The ICFP 2010 talks are online for some days … hours and hours of home entertainment! Here is the presentation of my favorite ICFP 2010 paper:
And here is my own stressed and tired talk (for a less stressed version see this):
It’s amazing how much you can learn from a video of your own talk. So many times your impression as a speaker about what the audience got out of your talk are completely off. I wish more conferences would record talks, then maybe the talks would get better.
September 23, 2010
DVerify is a new tool for verifying Dminor programs. It achieves pretty much the same thing as the Dminor type-checker, just in a quite different way: DVerify translates Dminor programs into a quite standard while language, and then uses the Boogie generic verification condition generator backend to verify the translated program. The soundness of this technique has been proved formally using Coq. DVerify and the Coq proofs are the product of Thorsten Tarrach’s recently defended Master’s thesis.
September 20, 2010
Today we released version 0.1.1 of Dminor, our type-checker for a subset of the code name “M” Modeling Language. This brings several bug fixes and a couple of optimizations to our semantic-subtyping-based prototype type-checker. Andy Gordon posted about the original release of Dminor in December.
September 8, 2010
“Computational functions are reflected, at the logical level, as pairs of a precondition and postcondition. [...] A function’s precondition and postcondition alone determine how it is lifted: its code is ignored. (The conformance of a function’s body to its declared pre- and postcondition
is checked, of course, via a proof obligation [...]) This reflects a philosophy in which the only way of reasoning about the behavior of a function value is via its specification: code never appears within formulae.” — It seems that it took a very long time until this extremely natural idea was finally incorporated in a decent Hoare logic for functional programs (and a couple more years until it finally reached the world of refinement type systems )
“In this paper, we [...] allow specifications to be expressed in higher-order logic. The intuitive justification for this approach is that, if functions can abstract over functions, then specifications must abstract over specifications.”
September 7, 2010
I’ve run across some recent papers relating type systems and software model-checking, and I find this subject quite fascinating – even more when I think that my student, Thorsten, has just submitted his thesis on a somehow related topic (he’s relating a type system to a verification condition generator), without even knowing about the existence of all this related work.
I will read more! I will read more! I will read more!
November 13, 2008
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.
December 20, 2007
Here is the final version of the paper I wrote with Jan as a follow up of my Master’s thesis. I’ll present it at the Workshop on Foundations of Object-Oriented Languages (FOOL’08) on the 13th January in San Francisco. This means I will also attend POPL, with which the workshop is affiliated, and I’m quite excited about it. Anyway, here is the paper and the 64-page extended version with full proofs.
Since the workshop does not count as prior publication the next step for us is to submit a slightly improved version to the Logical Methods in Computer Science journal.
June 16, 2007
- Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. Symbolic Execution with Separation Logic. APLAS 2005.
- Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. A Local Shape Analysis based on Separation Logic. TACAS 2006.
- Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O’Hearn, Thomas Wies, and Hongseok Yang. Shape analysis for composite data structures. CAV 2007.
Reading one paper each day, makes the doctor go away