This page contains the Coq development accompanying the following article:
Xavier Leroy and Hervé Grall, Coinductive big-step operational semantics, 2007. Submitted for publication. Extended version of the paper with the same title published in the proceedings of ESOP 2006.
Coq source files:
semantics.v |
Big-step and small-step semantics; equivalence results (sections 3, 4, 7.1, 7.2 of the paper) |
densem.v |
Connections with denotational semantics (section 5) |
traces.v |
Extension to trace semantics (section 6) |
cps.v |
Coevaluation for CPS terms (section 7.3) |
typing.v |
Application to type soundness proofs (section 8) |
compilation.v |
Application to compiler correctness proofs (section 9) |
A .tgz archive of the Coq sources.
Require Coq version 8.1 or later.