Conference ProceedingsOPEN ACCESS

Coinductive big-step operational semantics

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2006) 3924 LNCS 54-68
DOI: 10.1007/11693024_5
22Citations
Citations of this article
3Readers
Mendeley users who have this article in their library.

Abstract

This paper illustrates the use of coinductive 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. © Springer-Verlag Berlin Heidelberg 2006.

Cite

CITATION STYLE

APA

Leroy, X. (2006). Coinductive big-step operational semantics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3924 LNCS, pp. 54–68). https://doi.org/10.1007/11693024_5

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free