Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking.

Abstract : In the book on Advanced Topics in Types and Programming Languages, Crary illustrates the reasoning method of logical relations in a case study about equivalence checking. He presents a type-driven equivalence checking algorithm and verifies its completeness with respect to a definitional characterisation of equivalence. We present in this paper a formalisation of Crary's proof using Isabelle/HOL and the nominal datatype package.
Type de document :
Communication dans un congrès
Brigitte Pientka and Carsten Schürmann. LFMTP'07, Jul 2007, Bremen, Germany. Elsevier, 196, 15p., 2008, ENTCS. 〈10.1016/j.entcs.2007.09.014〉
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00180061
Contributeur : Julien Narboux <>
Soumis le : mardi 29 juin 2010 - 13:50:44
Dernière modification le : mercredi 30 juin 2010 - 08:33:46
Document(s) archivé(s) le : jeudi 1 décembre 2016 - 06:09:52

Fichier

lfmtp-07.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Julien Narboux, Christian Urban. Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking.. Brigitte Pientka and Carsten Schürmann. LFMTP'07, Jul 2007, Bremen, Germany. Elsevier, 196, 15p., 2008, ENTCS. 〈10.1016/j.entcs.2007.09.014〉. 〈inria-00180061v2〉

Partager

Métriques

Consultations de la notice

50

Téléchargements de fichiers

61