Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation

DOI10.1093/LOGCOM/13.5.689zbMATH Open1036.03036OpenAlexW2012956948MaRDI QIDQ4444936FDOQ4444936

Authors: Roy Dyckhoff, Christian Urban 

Publication date: 28 January 2004

Published in: Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/13.5.689

Recommendations

• Functional and Logic Programming
• Explicit substitution. On the edge of strong normalization
• Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi
• \(\lambda\)-calculi with explicit substitutions preserving strong normalization
• Completing Herbelin’s Programme

zbMATH Keywords

lambda-calculusstrong normalizationsequent calculusbeta-reductionexplicit substitutionminimal implicational logic

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Cited In (7)

• Functional and Logic Programming
• Title not available (Why is that?)
• Call-by-name reduction and cut-elimination in classical logic
• Pattern matching as cut elimination
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction
• A resource aware semantics for a focused intuitionistic calculus
• Cut elimination, substitution and normalisation

This page was built for publication: Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4444936)