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

DOI10.1007/3-540-56939-1_109MaRDI QIDQ4630299zbMATH OpenOpenAlexFDO

Authors Roberto Di Cosmo, Delia Kesner

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)

Recommendations

• Simulating expansions without expansions
• Extensional Rewriting with Sums
• scientific article; zbMATH DE number 176742
• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• A confluent reduction for the λ-calculus with surjective pairing and terminal object

Cites work

• 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?)
• An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus
• Combinatory logic. With two sections by William Craig.
• 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

(19)

• scientific article; zbMATH DE number 2185660 (Why is no real title available?)
• Strongly typed rewriting for coupled software transformation
• Simulating expansions without expansions
• Some lambda calculi with categorical sums and products
• Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract)
• Call-by-name extensionality and confluence
• Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
• Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• scientific article; zbMATH DE number 3954870 (Why is no real title available?)
• scientific article; zbMATH DE number 176742 (Why is no real title available?)
• Extensional Rewriting with Sums
• Isomorphisms of simple inductive types through extensional rewriting
• An upper bound for reduction sequences in the typed \(\lambda\)-calculus
• Equality between functionals in the presence of coproducts
• scientific article; zbMATH DE number 2185658 (Why is no real title available?)
• Combining first order algebraic rewriting systems, recursion and extensional lambda calculi
• A confluent reduction for the λ-calculus with surjective pairing and terminal object
• Rewriting with extensional polymorphic \(\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)