A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language

Adam Chlipala. A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI'07). June 2007.

Paper as PDF, Paper as PS


We present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational semantics assigned to the intermediate languages. We demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge large parts of our proof obligations automatically.

Software/proof source code and documentation

Slides are available from my PLDI talk in OpenOffice and PDF formats.

Slides are also available from a talk I gave at the Projet Gallium seminar at INRIA Rocquencourt, in OpenOffice and PDF formats.