Hereditary Substitutions for Simple Types, Formalized

Chantal Keller 1, 2, 3 Thorsten Altenkirch 4
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : We analyze a normalization function for the simply typed lambda-calculus based on hereditary substitutions, a technique developed by Pfenning et al. The normalizer is implemented in Agda, a total language where all programs terminate. It requires no termination proof since it is structurally recursive which is recognized by Agda's termination checker. Using Agda as an interactive theorem prover we establish that our normalization function precisely identifies beta-eta-equivalent terms and hence can be used to decide beta-eta-equality. An interesting feature of this approach is that it is clear from the construction that beta-\eta-equality is primitive recursive.
Type de document :
Communication dans un congrès
Capretta, V. and Chapman, J. MSFP - Third Workshop on Mathematically Structured Functional Programming - 2010, Sep 2010, Baltimore, United States. ACM Press, 2010, Proceedings of the Mathematically Structured Functional Programming workshop, ACM Press 2010, Baltimore, Marylan, USA, September 25, 2010
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00520606
Contributeur : Chantal Keller <>
Soumis le : mardi 20 mars 2012 - 11:36:59
Dernière modification le : jeudi 10 mai 2018 - 02:06:19
Document(s) archivé(s) le : lundi 26 novembre 2012 - 11:35:18

Fichier

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

Identifiants

  • HAL Id : inria-00520606, version 1

Collections

Citation

Chantal Keller, Thorsten Altenkirch. Hereditary Substitutions for Simple Types, Formalized. Capretta, V. and Chapman, J. MSFP - Third Workshop on Mathematically Structured Functional Programming - 2010, Sep 2010, Baltimore, United States. ACM Press, 2010, Proceedings of the Mathematically Structured Functional Programming workshop, ACM Press 2010, Baltimore, Marylan, USA, September 25, 2010. 〈inria-00520606〉

Partager

Métriques

Consultations de la notice

315

Téléchargements de fichiers

251