Coinductive big-step operational semantics

Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/inria-00289545
Contributor : Xavier Leroy <>
Submitted on : Saturday, June 21, 2008 - 1:44:42 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Friday, September 28, 2012 - 4:25:58 PM

Files

Identifiers

Collections

Citation

Xavier Leroy. Coinductive big-step operational semantics. European Symposium on Programming (ESOP 2006), Mar 2006, Vienne, Austria. pp.42-54, ⟨10.1007/11693024_5⟩. ⟨inria-00289545⟩

Share

Metrics

Record views

259

Files downloads

324