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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Berarducci, A., Dezani-Ciancaglini, M.: Infinite lambda-calculus and types. Theor. Comp. Sci. 212(1-2), 29–75 (1999)
Bertot, Y.: Filters on coinductive streams, an application to Eratosthenes’ sieve. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 102–115. Springer, Heidelberg (2005)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development – Coq’Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, Heidelberg (2004)
Cousot, P., Cousot, R.: Inductive definitions, semantics and abstract interpretation. In: 19th symp. Principles of Progr. Lang., pp. 83–94. ACM Press, New York (1992)
Gapeyev, V., Levin, M., Pierce, B.: Recursive subtyping revealed. J. Func. Progr. 12(6), 511–548 (2003)
Giménez, E.: Codifying guarded definitions with recursive schemes. In: Smith, J., Dybjer, P., Nordström, B. (eds.) TYPES 1994. LNCS, vol. 996, pp. 39–59. Springer, Heidelberg (1995)
Grall, H.: Deux critères de sécurité pour léxécution de code mobile. PhD thesis, École Nationale des Ponts et Chaussées (December 2003)
Grégoire, B.: Compilation des termes de preuves: un (nouveau) mariage entre Coq et OCaml. PhD thesis, University Paris 7 (2003)
Gunter, C.A., Rémy, D.: A proof-theoretic assessment of runtime type errors. Research Report 11261-921230-43TM, AT&T Bell Laboratories (1993)
Hardin, T., Maranget, L., Pagano, B.: Functional runtimes within the lambdasigma calculus. Journal of Functional Programming 8(2), 131–176 (1998)
Kennaway, R., Klop, J.W., Sleep, M.R., de Vries, F.-J.: Infinitary lambda calculus. Theor. Comp. Sci. 175(1), 93–125 (1997)
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. Technical Report 0400001T.1, National ICT Australia (March 2004) (To appear in ACM TOPLAS)
Leroy, X.: Coinductive big-step operational semantics – the Coq development (2005), Available from pauillac.inria.fr/~xleroy
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd symp. Principles of Progr. Lang., pp. 42–54. ACM Press, New York (2006)
Leroy, X., Rouaix, F.: Security properties of typed applets. In: Vitek, J. (ed.) Secure Internet Programming. LNCS, vol. 1603, pp. 147–182. Springer, Heidelberg (1999)
Milner, R., Tofte, M.: Co-induction in relational semantics. Theor. Comp. Sci. 87, 209–220 (1991)
Rittri, M.: Proving the correctness of a virtual machine by a bisimulation. Licentiate thesis, Göteborg University (1988)
Stoughton, A.: An operational semantics framework supporting the incremental construction of derivation trees. In: Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II). Electronic Notes in Theoretical Computer Science, vol. 12, Elsevier, Amsterdam (1998)
Strecker, M.: Compiler verification for C0. Technical report, Université Paul Sabatier, Toulouse (April 2005)
Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. and Comp. 115(1), 38–94 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leroy, X. (2006). Coinductive Big-Step Operational Semantics. In: Sestoft, P. (eds) Programming Languages and Systems. ESOP 2006. Lecture Notes in Computer Science, vol 3924. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11693024_5
Download citation
DOI: https://doi.org/10.1007/11693024_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33095-0
Online ISBN: 978-3-540-33096-7
eBook Packages: Computer ScienceComputer Science (R0)