The permutative lambda calculus - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

The permutative lambda calculus

Résumé

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.
Fichier principal
Vignette du fichier
LPAR2012.pdf (250.52 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00780361 , version 1 (23-01-2013)

Identifiants

  • HAL Id : hal-00780361 , version 1

Citer

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. ⟨hal-00780361⟩
209 Consultations
263 Téléchargements

Partager

Gmail Facebook X LinkedIn More