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

DOI10.1017/S0956796800001696zbMath0856.68087OpenAlexW2067383648MaRDI QIDQ4895554

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

rewriting systemspolymorphic types

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items

Kleene Monads: Handling Iteration in a Framework of Generic Effects

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
• On the implementation of abstract data types by programming language constructs
• Strong normalization for typed terms with surjective pairing
• Algebra of constructions. I. The word problem for partial algebras
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• Characterization of normal forms possessing inverse in the \(\lambda\)- \(\beta\)-\(\eta\)-calculus
• Provable isomorphisms of types
• Recognizable sets of graphs: equivalent definitions and closure properties
• The virtues of eta-expansion
• Intensional interpretations of functionals of finite type I