Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL

DOI10.1016/0304-3975(89)90105-9zbMath0707.03012OpenAlexW2095553492MaRDI QIDQ918956

Thérèse Hardin

Publication date: 1989

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(89)90105-9

zbMATH Keywords

rewriting systems\(\lambda \) -calculus with surjective pairingCartesian Closed CategoriesCategorical Combinatory Logicconfluence propertieslocally confluent subsystem

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Grammars and rewriting systems (68Q42) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Combinatory logic and lambda calculus (03B40)

Related Items (16)

Eta-conversion for the languages of explicit substitutions ⋮ On confluence for weakly normalizing systems ⋮ Explicit substitutions with de bruijn's levels ⋮ On explicit substitution with names ⋮ Church-Rosser theorem for a rewriting system on categorical combinators ⋮ On explicit substitutions and names (extended abstract) ⋮ A notation for lambda terms. A generalization of environments ⋮ Pure type systems with explicit substitutions ⋮ A confluent reduction for the λ-calculus with surjective pairing and terminal object ⋮ The spirit of node replication ⋮ Explicit substitutions ⋮ λν, a calculus of explicit substitutions which preserves strong normalisation ⋮ An abstract framework for environment machines ⋮ A categorical understanding of environment machines ⋮ Theoretical Pearl Yet yet a counterexample for λ+SP ⋮ Strong normalization of substitutions

Cites Work

• Church-Rosser theorem for a rewriting system on categorical combinators
• Proof of termination of the rewriting system SUBSET on CCL
• Pairing Without Conventional Restraints
• A new implementation technique for applicative languages
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL