Coinductive big-step operational semantics

Xavier Leroy 1
1 GALLIUM - Programming languages, types, compilation and proofs
Inria Paris-Rocquencourt
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.
Type de document :
Communication dans un congrès
Peter Sestoft. European Symposium on Programming (ESOP 2006), Mar 2006, Vienne, Austria. Springer, 3924, pp.42-54, 2006, Lecture Notes in Computer Science. 〈10.1007/11693024_5〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00289545
Contributeur : Xavier Leroy <>
Soumis le : samedi 21 juin 2008 - 13:44:42
Dernière modification le : lundi 5 octobre 2015 - 16:58:39
Document(s) archivé(s) le : vendredi 28 septembre 2012 - 16:25:58

Fichiers

coindsem.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA

Citation

Xavier Leroy. Coinductive big-step operational semantics. Peter Sestoft. European Symposium on Programming (ESOP 2006), Mar 2006, Vienne, Austria. Springer, 3924, pp.42-54, 2006, Lecture Notes in Computer Science. 〈10.1007/11693024_5〉. 〈inria-00289545〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de
la notice

202

Téléchargements du document

184

Contact


archive-ouverte@inria.fr