Category: Semantics and Compilation
Compilation
- CompCert: CompCert, a Certified C Compiler
Xavier Leroy
- DistributedReferenceCounting: A Construction of Distributed Reference Counting
Luc Moreau, Jean Duprat
- GC: Formal Verification of an Incremental Garbage Collector
Solange Coupet-Grimal and Catherine Nouvet
- MiniCompiler: Correctness of a tiny compiler for arithmetic expressions
Jean-Christophe Filliâtre
- MiniML: Correctness of the compilation of Mini-ML into the Categorical Abstract Machine
Samuel Boutin
- RelationExtraction: Functions extraction from inductive relations
Catherine Dubois, David Delahaye, Pierre-Nicolas Tollitte
Semantics
- Continuations: A toolkit to reason with programs raising exceptions
Jean-François Monin
- Exceptions: Pro[gramm,v]ing with continuations:A development in Coq.
Pierre Castéran
- HoareTut: A Tutorial on Reflecting in Coq the generation of Hoare proof obligations
Sylvain Boulmé
- IEEE754: A formalisation of the IEEE754 norm on floating-point arithmetic
Patrick Loiseleur
- Kildall: Application of the Generic kildall's Data Flow Analysis Algorithm to a Type and Shape Static Analyses of Bytecode
Solange Coupet-Grimal, William Delobel
- MiniC: Semantics of a subset of the C language
Eduardo Giménez and Emmanuel Ledinot
- Semantics: A survey of semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, to
abstract interpretation.
Yves Bertot