zbMATH — the first resource for mathematics

Strong normalization proof with CPS-translation for second order classical natural deduction. (English) Zbl 1058.03060
J. Symb. Log. 68, No. 3, 851-859 (2003); Corrigendum ibid. 68, No. 4, 1415-1416 (2003).
Summary: This paper points out an error of Parigot’s proof of strong normalization of second-order classical natural deduction by the CPS-translation [M. Parigot, J. Symb. Log. 62, No. 4, 1461–1479 (1997; Zbl 0941.03063)], discusses erasing-continuation of the CPS-translation, and corrects that proof by using the notion of augmentations.
From the text of the Corrigendum: Our paper contains a serious error. Proposition 4.6 is actually false and hence our strong normalization proof does not work for the Curry-style $$\lambda\mu$$-calculus. However, our method still can show (1) the correction of Proposition 5.4 of Parigot’s paper and (2) the correction of the proof of strong normalization of Church-style $$\lambda\mu$$-calculus by CPS translation.

MSC:
 03F05 Cut-elimination and normal-form theorems 03B40 Combinatory logic and lambda calculus
Full Text:
References:
 [1] P. de Groote A CPS -translation for the $$\lambda\mu$$-calculus, Lecture Notes in Computer Science, vol. 787, Springer-Verlag,1994. · Zbl 0938.03024 [2] K. Fujita Domain-free $$\lambda\mu$$-calculus , Theoretical Informatics and Applications , vol. 34 (2000), pp. 433–466. · Zbl 0974.68032 · doi:10.1051/ita:2000102 · eudml:222038 [3] J.-Y. Girard, P. Taylor, and Y. Lafont Proofs and types , Cambridge University Press,1989. · Zbl 0671.68002 [4] K. Nakazawa Confluency and strong normalizability of call-by-value $$\lambda\mu$$-calculus , Theoretical Computer Science , vol. 290 (2003), no. 1, pp. 429–463. · Zbl 1018.68016 · doi:10.1016/S0304-3975(01)00380-2 [5] M. Parigot $$\lambda\mu$$-calculus: an algorithmic interpretation of natural deduction, Proceedings of the international conference on logic programming and automated reasoning , Lecture Notes in Computer Science, vol. 624, Springer-Verlag,1992, pp. 190–201. · Zbl 0925.03092 [6] G. D. Plotkin Call-by-name, call-by-value and the $$\lambda$$-calculus , Theoretical Computer Science , vol. 1 (1975), pp. 125–159. · Zbl 0325.68006 · doi:10.1016/0304-3975(75)90017-1
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.