scientific article; zbMATH DE number 176742

MaRDI QIDQ4036571zbMATHFDO

Authors Pierre-Louis Curien, Roberto Di Cosmo

Publication date 18 May 1993

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)

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

Cited in

(18)

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

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)