scientific article
zbMATH Open0769.68056MaRDI QIDQ4036571FDOQ4036571
Roberto Di Cosmo, Pierre-Louis Curien
Publication date: 18 May 1993
Title of this publication is not available (Why is that?)
decidabilityterminal objectpolymorphic typesconfluent rewriting system\(\lambda\)-calculus extended with surjective pairingfull equational theory underlying cartesian closed categoriespolymorphic extensions
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 (13)
- Rewriting with extensional polymorphic \(\lambda \)-calculus
- 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
- Structures definable in polymorphism
- Subtyping + extensionality: Confluence of βηtop reduction in F≤
- 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
- A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object
- Some lambda calculi with categorical sums and products
Recommendations
- Title not available (Why is that?) 👍 👎
- Title not available (Why is that?) 👍 👎
- Confluence of the coinductive \(\lambda\)-calculus 👍 👎
- A Terminating and Confluent Linear Lambda Calculus 👍 👎
- A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object 👍 👎
- Reduction rules for intuitionistic \(\lambda\rho\)-calculus 👍 👎
- Reducibility Proofs in the λ-Calculus 👍 👎
- Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative 👍 👎
- A confluent reduction for the λ-calculus with surjective pairing and terminal object 👍 👎
- The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type 👍 👎
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)
