TY - GEN
T1 - The permutative λ-calculus
AU - Accattoli, Beniamino
AU - Kesner, Delia
PY - 2012/3/21
Y1 - 2012/3/21
N2 - We introduce the permutative λ-calculus, an extension of λ-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 λ-terms.
AB - We introduce the permutative λ-calculus, an extension of λ-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 λ-terms.
U2 - 10.1007/978-3-642-28717-6_5
DO - 10.1007/978-3-642-28717-6_5
M3 - Conference contribution
AN - SCOPUS:84858328289
SN - 9783642287169
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 23
EP - 36
BT - Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Proceedings
T2 - 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-18
Y2 - 11 March 2012 through 15 March 2012
ER -