Proof pearl: abella formalization of lambda-calculus cube property

Beniamino Accattoli 1, 2
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : In 1994 Gerard Huet formalized in Coq the cube property of lambda-calculus residuals. His development is based on a clever idea, a beautiful inductive definition of residuals. However, in his formalization there is a lot of noise concerning the representation of terms with binders. We re-interpret his work in Abella, a recent proof assistant based on higher-order abstract syntax and provided with a nominal quantifier. By revisiting Huet's approach and exploiting the features of Abella, we get a strikingly compact and natural development, which makes Huet's idea really shine.
Type de document :
Communication dans un congrès
Second international conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. 2012
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00780337
Contributeur : Beniamino Accattoli <>
Soumis le : mercredi 23 janvier 2013 - 17:18:09
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : mercredi 24 avril 2013 - 03:59:41

Fichier

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

Identifiants

  • HAL Id : hal-00780337, version 1

Collections

Citation

Beniamino Accattoli. Proof pearl: abella formalization of lambda-calculus cube property. Second international conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. 2012. 〈hal-00780337〉

Partager

Métriques

Consultations de la notice

188

Téléchargements de fichiers

109