Proof of termination of the rewriting system SUBSET on CCL

DOI10.1016/0304-3975(86)90035-6zbMath0618.68031OpenAlexW1970547272MaRDI QIDQ1822494

Alain Laville, Thérèse Hardin

Publication date: 1986

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

Full work available at URL: https://doi.org/10.1016/0304-3975(86)90035-6

zbMATH Keywords

rewriting system\(\lambda \) c-calculusPure Combinatory Categorical Logic

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Related Items (14)

Termination of term rewriting by interpretation ⋮ Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract) ⋮ Categorical abstract machines for higher-order typed \(\lambda\)-calculi ⋮ Church-Rosser theorem for a rewriting system on categorical combinators ⋮ Maximal Termination ⋮ Alpha conversion, conditions on variables and categorical logic ⋮ Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL ⋮ Explicit Substitutions à la de Bruijn ⋮ Explicit substitutions ⋮ Termination by completion ⋮ Unnamed Item ⋮ Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions ⋮ A categorical understanding of environment machines ⋮ Strong normalization of substitutions

Uses Software

• REVE

Cites Work

• Orderings for term-rewriting systems
• Termination by completion
• Proving termination with multiset orderings
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proof of termination of the rewriting system SUBSET on CCL