Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-00780361
Contributor : Beniamino Accattoli <>
Submitted on : Wednesday, January 23, 2013 - 5:46:29 PM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Wednesday, April 24, 2013 - 4:00:20 AM

File

LPAR2012.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-00780361⟩

Share

Metrics

Record views

412

Files downloads

260