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.
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