Explicit substitution. On the edge of strong normalization

DOI10.1016/S0304-3975(97)00183-7zbMath0913.68130MaRDI QIDQ1274458

Roel Bloo, Herman Geuvers

Publication date: 12 January 1999

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

zbMATH Keywords

lambda-calculusexplicit substitutionrecursive path order

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Related Items

Intersection types for explicit substitutions ⋮ On explicit substitution with names ⋮ Resource operators for \(\lambda\)-calculus ⋮ Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting ⋮ Call-by-name reduction and cut-elimination in classical logic ⋮ Lambda-calculus with director strings ⋮ Strong Normalisation of Cut-Elimination That Simulates β-Reduction

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A note on simplification orderings
• λ-calculi with explicit substitutions and composition which preserve β-strong normalization
• λν, a calculus of explicit substitutions which preserves strong normalisation
• ON STEPWISE EXPLICIT SUBSTITUTION
• Explicit substitutions
• Combinatory reduction systems with explicit substitution that preserve strong normalisation