scientific article; zbMATH DE number 176742

zbMATH Open0769.68056MaRDI QIDQ4036571FDOQ4036571

Authors: Pierre-Louis Curien, Roberto Di Cosmo 

Publication date: 18 May 1993

Title of this publication is not available (Why is that?)

Recommendations

• A confluent reduction for the λ-calculus with surjective pairing and terminal object
• A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
• The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
• Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative
• Publication:3202990
• Reduction rules for intuitionistic \(\lambda\rho\)-calculus
• Publication:4945227
• Confluence of the coinductive \(\lambda\)-calculus
• Reducibility Proofs in the λ-Calculus
• A Terminating and Confluent Linear Lambda Calculus

zbMATH Keywords

decidabilityterminal objectpolymorphic typesconfluent rewriting system\(\lambda\)-calculus extended with surjective pairingfull equational theory underlying cartesian closed categoriespolymorphic extensions

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Cited In (18)

• Title not available (Why is that?)
• Rewriting with extensional polymorphic \(\lambda \)-calculus
• Title not available (Why is that?)
• Embedding of a free cartesian-closed category into the category of sets
• Title not available (Why is that?)
• Categorical abstract machines for higher-order typed \(\lambda\)-calculi
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• Unique normal forms for lambda calculus with surjective pairing
• A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
• Structures definable in polymorphism
• 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
• Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract)
• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Subtyping + extensionality: confluence of \(\beta \eta\)top reduction in \(\mathrm{F}_\leq\)
• Some lambda calculi with categorical sums and products
• Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
• Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative

This page was built for publication:

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