This page contains the Coq development accompanying the following article:
Xavier Leroy and Hervé Grall, Coinductive big-step operational semantics, Information and Computation 207(2):284-304, 2009. Extended version of the paper with the same title published in the proceedings of ESOP 2006.
Pretty-printed Coq sources:
semantics |
Big-step and small-step semantics; equivalence results (sections 3, 4, 7.1, 7.2 of the paper) |
densem |
Connections with denotational semantics (section 5) |
traces |
Extension to trace semantics (section 6) |
cps |
Coevaluation for CPS terms (section 7.3) |
typing |
Application to type soundness proofs (section 8) |
compilation |
Application to compiler correctness proofs (section 9) |
A .tgz archive of the Coq sources.
For Coq version 8.11 or later.
(For older Coq versions, try the previous archive.)
Copyright 2005, 2006, 2007, 2020 Institut National de Recherche en Informatique et Automatique (INRIA). These files are distributed under the terms of the GNU Public License version 2.