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.
The Compcert verified compiler
Compcert is a moderately optimizing compiler from most of the ISO C 1999 language to PowerPC, ARM and x86 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. Commercial versions are available from AbsInt.
Useful Coq libraries
- Coqlib: Coq sources and pretty-printed source
- Provides some tactics, definitions and lemmas on lists, positive integers and integers that I use a lot.
- 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'.
A locally nameless solution to the POPLmark challenge
Technical report and Coq sources
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.
The Listmachine benchmark
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.
Coinductive big-step semantics
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.
A memory model for C-like languages
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.
Compilation of parallel moves
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.
Higher-order uncurrying
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.