| HAL-Inria | Publications, software ... of Inria's scientists |
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.
Cited literature [19 references]
https://hal.inria.fr/inria-00289545
Contributor : Xavier Leroy <>
Submitted on : Saturday, June 21, 2008 - 1:44:42 PM
Last modification on : Tuesday, December 8, 2020 - 10:50:49 AM
Long-term archiving on: : Friday, September 28, 2012 - 4:25:58 PM
Contributor : Xavier Leroy <>
Submitted on : Saturday, June 21, 2008 - 1:44:42 PM
Last modification on : Tuesday, December 8, 2020 - 10:50:49 AM
Long-term archiving on: : Friday, September 28, 2012 - 4:25:58 PM