Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
From MaRDI portal
Publication:918956
DOI10.1016/0304-3975(89)90105-9zbMath0707.03012OpenAlexW2095553492MaRDI QIDQ918956
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
rewriting systems\(\lambda \) -calculus with surjective pairingCartesian Closed CategoriesCategorical Combinatory Logicconfluence propertieslocally confluent subsystem
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
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
