A confluent reduction for the extensional typed -calculus with pairs, sums, recursion and terminal object
From MaRDI portal
(Redirected from Publication:4630299)
A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
Recommendations
Cites work
- An algebraic interpretation of the K-calculus; and an application of a labelled -calculus
- Combinatory logic. With two sections by William Craig.
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 3730111 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 176742 (Why is no real title available?)
- scientific article; zbMATH DE number 3573844 (Why is no real title available?)
- scientific article; zbMATH DE number 512797 (Why is no real title available?)
- scientific article; zbMATH DE number 3358455 (Why is no real title available?)
- On the implementation of abstract data types by programming language constructs
- Simulating expansions without expansions
- Strong normalization for typed terms with surjective pairing
- The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
- The lambda calculus. Its syntax and semantics. Rev. ed.
- The virtues of eta-expansion
Cited in
(21)- Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
- Equality between functionals in the presence of coproducts
- An upper bound for reduction sequences in the typed -calculus
- Strongly typed rewriting for coupled software transformation
- scientific article; zbMATH DE number 2185658 (Why is no real title available?)
- scientific article; zbMATH DE number 2185660 (Why is no real title available?)
- Isomorphisms of simple inductive types through extensional rewriting
- Extensional Rewriting with Sums
- scientific article; zbMATH DE number 3954870 (Why is no real title available?)
- scientific article; zbMATH DE number 176742 (Why is no real title available?)
- scientific article; zbMATH DE number 1332635 (Why is no real title available?)
- Simulating expansions without expansions
- Combining first order algebraic rewriting systems, recursion and extensional lambda calculi
- A confluent reduction for the λ-calculus with surjective pairing and terminal object
- 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
- The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
- Call-by-name extensionality and confluence
- Rewriting with extensional polymorphic \(\lambda \)-calculus
- Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus
This page was built for publication: A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4630299)
