Coinductive big-step operational semantics - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2006

Coinductive big-step operational semantics

Xavier Leroy
Programming languages, types, compilation and proofs

Résumé

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.

Domaines

Langage de programmation [cs.PL]
Fichier principal
Vignette du fichier
coindsem.pdf (135.63 Ko) Télécharger le fichier
compilation.v (12.57 Ko) Télécharger le fichier
semantics.v (15.56 Ko) Télécharger le fichier
typing.v (12.2 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Format : Autre
Format : Autre
Format : Autre

Xavier Leroy  : Connectez-vous pour contacter le contributeur

https://inria.hal.science/inria-00289545

Soumis le : samedi 21 juin 2008-13:44:42

Dernière modification le : jeudi 3 février 2022-11:18:23

Archivage à long terme le : vendredi 28 septembre 2012-16:25:58

Télécharger pour visualiser

Dates et versions

inria-00289545 , version 1 (21-06-2008)

Identifiants

Citer

Xavier Leroy. Coinductive big-step operational semantics. European Symposium on Programming (ESOP 2006), Mar 2006, Vienne, Austria. pp.42-54, ⟨10.1007/11693024_5⟩. ⟨inria-00289545⟩

Exporter

BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

INRIA INRIA2 ANR
109 Consultations
317 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More