Xavier Leroy. Coinductive big-step operational semantics. In ESOP 2006: European Symposium on Programming, number 3924 in LNCS, pages 54--68. Springer, 2006.

This paper illustrates the use of co-inductive definitions and proofs in big-step operational semantics, enabling the latter to describe diverging evaluations in addition to terminating evaluations. We show applications to proofs of type soundness and to proofs of semantic preservation for compilers. (See http://gallium.inria.fr/~xleroy/publi/coindsem/ for the Coq on-machine formalization of these results.)

bib | DOI | Local copy | At publisher's site ] Back

This file was generated by bibtex2html 1.99.