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

DOI10.1093/logcom/13.5.689zbMath1036.03036OpenAlexW2012956948MaRDI QIDQ4444936

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

sequent calculusstrong normalizationlambda-calculusbeta-reductionexplicit substitutionminimal implicational logic

Mathematics Subject Classification ID

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

Related Items (5)

Pattern matching as cut elimination ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ Call-by-name reduction and cut-elimination in classical logic ⋮ 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