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

DOI10.1093/LOGCOM/13.5.689MaRDI QIDQ4444936zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(7)

• A resource aware semantics for a focused intuitionistic calculus
• scientific article; zbMATH DE number 2086241 (Why is no real title available?)
• Functional and Logic Programming
• Call-by-name reduction and cut-elimination in classical logic
• Pattern matching as cut elimination
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction
• 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)