The permutative lambda calculus

Abstract : We introduce the permutative lambda-calculus, an extension of lambda-calculus with three equations and one reduction rule for permuting constructors, generalising many calculi in the literature, in particular Regnier's sigma-equivalence and Moggi's assoc-equivalence. We prove confluence modulo the equations and preservation of beta-strong normalisation (PSN) by means of an auxiliary substitution calculus. The proof of confluence relies on M-developments, a new notion of development for lambda-terms.
Type de document :
Communication dans un congrès
18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR-18, Mar 2012, Merida, Venezuela. 2012
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00780361
Contributeur : Beniamino Accattoli <>
Soumis le : mercredi 23 janvier 2013 - 17:46:29
Dernière modification le : jeudi 15 novembre 2018 - 20:27:00
Document(s) archivé(s) le : mercredi 24 avril 2013 - 04:00:20

Fichier

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

Identifiants

  • HAL Id : hal-00780361, version 1

Collections

Citation

Beniamino Accattoli, Delia Kesner. The permutative lambda calculus. 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR-18, Mar 2012, Merida, Venezuela. 2012. 〈hal-00780361〉

Partager

Métriques

Consultations de la notice

362

Téléchargements de fichiers

121