The Church-Rosser theorem for the typed lambda-calculus with pairing pairing

DOI10.1305/NDJFL/1093883461zbMATH Open0476.03026OpenAlexW2009987765MaRDI QIDQ1159627FDOQ1159627

Authors: Garrel Pottinger 

Publication date: 1981

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1305/ndjfl/1093883461

zbMATH Keywords

Church-Rosser theoremtyped and type-free combinatory systemstyped lambda-calculus with pairing and projection constants

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cited In (12)

• Adding algebraic rewriting to the untyped lambda calculus
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• Unique normal forms for lambda calculus with surjective pairing
• The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
• A confluent reduction for the λ-calculus with surjective pairing and terminal object
• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
• Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract)
• On confluence for weakly normalizing systems
• Simulating expansions without expansions
• Provable isomorphisms of types
• A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object
• Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type

This page was built for publication: The Church-Rosser theorem for the typed lambda-calculus with pairing pairing

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