A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object
From MaRDI portal
Publication:4630299
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
Related Items (8)
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
This page was built for publication: A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object
