This is the final release to go with the POPL'10 paper, focusing on the verified compiler from an impure Mini-ML language to an idealized assembly language.
Warning: This is the first release meant to work with Coq 8.2. Only the more recent examples (Untyped and Compose) have been verified to compile with 8.2.
Some old releases are still available.
|Composable theorems||Syntactic Proofs of Compositional Compiler Correctness||submitted draft|
|Impure languages||A Verified Compiler for an Impure Functional Language||POPL'10|
|Syntax & pure languages||Parametric Higher-Order Abstract Syntax for Mechanized Semantics||ICFP'08|
|Mostly-superceded initial work||A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language||PLDI'07|