The permutative lambda calculus

Beniamino Accattoli 1, 2 Delia Kesner 3
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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 10 mai 2018 - 02:06:57
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

350

Téléchargements de fichiers

120