HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/inria-00289545
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Saturday, June 21, 2008 - 1:44:42 PM
Last modification on : Thursday, February 3, 2022 - 11:18:23 AM
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

96

Files downloads

220