For several years, I have been using the Coq proof assistant to mechanize specifications and proofs in my research on programming languages and systems. This page collects some of my Coq developments, often accompanied with full Coq source and extensive commentaries. Unless otherwise mentioned, these developments are distributed under the terms of the GNU Public License version 2.
Compcert is a moderately optimizing compiler from a subset of the C language to PowerPC assembly language. It comes accompanied with a Coq proof of semantic preservation, ensuring that the generated assembly code behaves as prescribed by the source code. The whole Compcert development is available under a non-commercial licence.
- Coqlib: Coq sources and pretty-printed source
- Provides some tactics, definitions and lemmas on lists, positive integers and integers that are missing from the Coq standard library.
- Machine integers: Coq sources and pretty-printed source
- A fairly complete library for arithmetic and logical operations over N-bits machine integers.
- Mergesort: Coq sources and pretty-printed sources
- A sorting function for lists, developed using `Program'.
The POPLmark challenge is a collaborative experiment to assess the usability of theorem provers to conduct "POPL-style" research on semantics and type systems. My solution illustrates the use of the "locally nameless" representation for binders and bound variables.
Technical report and Coq and Twelf sources. Joint work with Andrew Appel.
In the spirit of POPLmark, Listmachine is a benchmark to compare theorem-proving systems on their ability to express proofs of compiler correctness. Andrew Appel and I constructed solutions in both Coq and Twelf metatheory.
Article and Coq sources. Joint work with Hervé Grall.
This work demonstrates the use of coinduction to define and reason about divergence (non-terminating executions) in big-step operational semantics. It is also an advanced tutorial on Coq's facilities for coinductive definitions and proofs.
Article and Coq sources. Joint work with Sandrine Blazy.
This work formalizes a memory model adequate for giving semantics to C-like programming languages and to compiler intermediate languages, and illustrates its uses to reason about compiler transformations of pointer programs. The memory model presented there generalizes the one used in the Compcert development.
Article and Coq sources. Joint work with Laurence Rideau and Bernard Paul Serpette.
The "parallel move" problem is the following: given a parallel assignment between variables (x1, ..., xn) = (y1, ..., yn) , where some variables can be used both as sources and destinations, find an equivalent sequence of elementary assignments x = y that uses as few temporaries as possible. This problem occurs in Compcert when enforcing calling conventions for functions. While efficient algorithms to solve this problem have been known since the 1970's, their proof of correctness is surprisingly difficult.
Article and Coq sources. Joint work with Zaynah Dargaye.
Uncurrying is an important optimization for the efficient execution of functional programming. We develop a generic framework to describe higher-order uncurrying optimizations and prove their correctness. The proof uses step-indexed logical relations, a powerful semantic tool.