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