The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
From MaRDI portal
Publication:1159627
DOI10.1305/ndjfl/1093883461zbMath0476.03026OpenAlexW2009987765MaRDI QIDQ1159627
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
Church-Rosser theoremtyped and type-free combinatory systemstyped lambda-calculus with pairing and projection constants
Related Items
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
