A confluent reduction for the λ-calculus with surjective pairing and terminal object

DOI10.1017/S0956796800001696MaRDI QIDQ4895554zbMATH OpenOpenAlexFDO

Authors Pierre-Louis Curien, Roberto Di Cosmo

Publication date 14 October 1996

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0956796800001696

zbMATH Keywords

polymorphic typesrewriting systems

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Recommendations

• scientific article; zbMATH DE number 176742
• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
• A confluent reduction for the extensional typed -calculus with pairs, sums, recursion and terminal object
• The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
• scientific article; zbMATH DE number 742724

Cites work

• Algebra of constructions. I. The word problem for partial algebras
• Characterization of normal forms possessing inverse in the - --calculus
• Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• Intensional interpretations of functionals of finite type I
• On the implementation of abstract data types by programming language constructs
• Provable isomorphisms of types
• Recognizable sets of graphs: equivalent definitions and closure properties
• 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

(9)

• Unique normal forms for lambda calculus with surjective pairing
• Kleene monads: handling iteration in a framework of generic effects
• scientific article; zbMATH DE number 176742 (Why is no real title available?)
• A confluent reduction for the extensional typed -calculus with pairs, sums, recursion and terminal object
• Normalisation of the TheoryTof Cartesian Closed Categories and Conservativity of ExtensionsT[x] ofT
• scientific article; zbMATH DE number 1841835 (Why is no real title available?)
• Some lambda calculi with categorical sums and products
• The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
• Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative

This page was built for publication: A confluent reduction for the λ-calculus with surjective pairing and terminal object

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4895554)