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

DOI10.1305/NDJFL/1093883461zbMath0476.03026OpenAlexW2009987765MaRDI QIDQ1159627

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)

Related Items (12)

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

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