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

DOI10.1305/NDJFL/1093883461MaRDI QIDQ1159627zbMATHOpenAlexFDO

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)

• Simulating expansions without expansions
• 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
• Adding algebraic rewriting to the untyped lambda calculus
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• On confluence for weakly normalizing systems
• The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
• A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
• Unique normal forms for lambda calculus with surjective pairing
• Provable isomorphisms of types
• A confluent reduction for the λ-calculus with surjective pairing and terminal object
• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)

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)