zbMATH — the first resource for mathematics

An isomorphism between cut-elimination procedure and proof reduction. (English) Zbl 1215.03067
Ronchi della Rocca, Simona (ed.), Typed lambda calculi and applications. 8th international conference, TLCA 2007, Paris, France, June 26–28, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73227-3/pbk). Lecture Notes in Computer Science 4583, 336-350 (2007).
Summary: This paper introduces a cut-elimination procedure of the intuitionistic sequent calculus and shows that it is isomorphic to the proof reduction of the intuitionistic natural deduction with general elimination and explicit substitution. It also proves strong normalization and Church-Rosser property of the cut-elimination procedure by projecting the sequent calculus to the natural deduction with general elimination without explicit substitution.
For the entire collection see [Zbl 1120.03002].

03F05 Cut-elimination and normal-form theorems
03B40 Combinatory logic and lambda calculus
Full Text: DOI