Formal SOS-Proofs for the Lambda-Calculus

Abstract : We describe in this paper formalisations for the properties of weakening, type-substitutivity, subject-reduction and termina- tion of the usual big-step evaluation relation. Our language is the lambda-calculus whose simplicity allows us to show actual theorem-prover code of the formal proofs. The formalisations are done in Nominal Isabelle, a de?nitional extention of the theorem prover Isabelle/HOL. The point of these formalisations is to be as close as possible to the ?pencil-and-paper? proofs for these properties, but of course be completely rigorous. We describe where Nominal Isabelle is of great help with such formalisations and where one has to invest additional effort in order to obtain formal proofs.
Type de document :
Communication dans un congrès
Third Workshop on Logical and Semantic Frameworks, with Applications, Aug 2008, Salvador, Brazil. Elsevier, 247, pp.139-155, 2009, ENTCS. 〈10.1016/j.entcs.2009.07.053〉
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-00335718
Contributeur : Julien Narboux <>
Soumis le : jeudi 30 octobre 2008 - 12:40:34
Dernière modification le : jeudi 11 janvier 2018 - 06:20:29
Document(s) archivé(s) le : mardi 9 octobre 2012 - 14:41:17

Fichier

SOS-lsfa08.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Christian Urban, Julien Narboux. Formal SOS-Proofs for the Lambda-Calculus. Third Workshop on Logical and Semantic Frameworks, with Applications, Aug 2008, Salvador, Brazil. Elsevier, 247, pp.139-155, 2009, ENTCS. 〈10.1016/j.entcs.2009.07.053〉. 〈inria-00335718〉

Partager

Métriques

Consultations de la notice

82

Téléchargements de fichiers

84