Strong normalisation of Herbelin's explicit substitution calculus

Abstract:

Cut elimination (in Gentzen's sequent calculus) and beta-reduction 
(in lambda calculus or, equivalently, natural deduction) are 
well-known to be similar processes but without an exact 
correspondence. Since about 1990, the lambda calculus has been 
enriched by the study of explicit substitution calculi, allowing 
beta-reductions to be interleaved with substitution reductions. 
Herbelin proposed in 1994 a calculus intermediate between sequent 
calculus and natural deduction, suitable like the former for proof 
search but without the permutabilities of Gentzen's calculus; he 
proposed a complete cut elimination system and showed it to be 
confluent and strongly normalising. Work described in the talk (joint 
work with C. Urban) shows how to extend this system with extra rules 
that allow the simulation of beta-reduction.