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

DOI10.1007/3-540-56939-1_109zbMATH Open1422.03022OpenAlexW1563667006MaRDI QIDQ4630299FDOQ4630299

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

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

zbMATH Keywords

proof theorycritical pairreduction systemreduction rulereduction sequence

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cites Work

• An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Simulating expansions without expansions
• The virtues of eta-expansion
• 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
• Title not available (Why is that?)

Cited In (19)

• Title not available (Why is that?)
• Rewriting with extensional polymorphic \(\lambda \)-calculus
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• Equality between functionals in the presence of coproducts
• Title not available (Why is that?)
• An upper bound for reduction sequences in the typed \(\lambda\)-calculus
• A confluent reduction for the λ-calculus with surjective pairing and terminal object
• Strongly typed rewriting for coupled software transformation
• Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract)
• Isomorphisms of simple inductive types through extensional rewriting
• Call-by-name extensionality and confluence
• Simulating expansions without expansions
• Combining first order algebraic rewriting systems, recursion and extensional lambda calculi
• Extensional Rewriting with Sums
• Title not available (Why is that?)
• Title not available (Why is that?)
• Some lambda calculi with categorical sums and products
• 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

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)