Coinductive big-step operational semantics

The Coq development

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.