zbMATH — the first resource for mathematics

A direct proof of strong normalization for an extended Herbelin’s calculus. (English) Zbl 1122.03311
Kameyama, Yukiyoshi (ed.) et al., Functional and logic programming. 7th international symposium, FLOPS 2004, Nara, Japan, April 7–9, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21402-X/pbk). Lecture Notes in Computer Science 2998, 244-259 (2004).
Summary: H. Herbelin [“A \(\lambda\)-caclulus structure isomorphic to Gentzen-style sequent calculus structure”, Lect. Notes Comput. Sci. 933, 61–75 (1995; Zbl 1044.03509)] presented an explicit substitution calculus with a sequent calculus as a type system, in which reduction steps correspond to cut-elimination steps. The calculus, extended with some rules for substitution propagation, simulates \(\beta \)-reduction of ordinary \(\lambda \)-calculus. In this paper we present a proof of strong normalization for the typable terms of the calculus. The proof is a direct one in the sense that it does not depend on the result of strong normalization for the simply typed \(\lambda \)-calculus, unlike an earlier proof by Dyckhoff and Urban.
For the entire collection see [Zbl 1048.68005].
Reviewer: Reviewer (Berlin)
03F05 Cut-elimination and normal-form theorems
03B40 Combinatory logic and lambda calculus
Full Text: DOI