Abstract
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. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Accattoli, B., & Kesner, D. (2012). The permutative λ-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7180 LNCS, pp. 23–36). https://doi.org/10.1007/978-3-642-28717-6_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
