A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object

DOI10.1007/3-540-56939-1_109zbMath1422.03022OpenAlexW1563667006MaRDI QIDQ4630299

Delia Kesner, Roberto Di Cosmo

Publication date: 29 March 2019

Published in: Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-56939-1_109

zbMATH Keywords

proof theorycritical pairreduction systemreduction rulereduction sequence

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

Some lambda calculi with categorical sums and products, Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract), Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type, Combining first order algebraic rewriting systems, recursion and extensional lambda calculi, Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus, Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions, Equality between functionals in the presence of coproducts, Strongly Typed Rewriting For Coupled Software Transformation

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• On the implementation of abstract data types by programming language constructs
• Strong normalization for typed terms with surjective pairing
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus
• Simulating expansions without expansions
• The virtues of eta-expansion