zbMATH — the first resource for mathematics

Strong normalization proofs by CPS-translations. (English) Zbl 1185.68625
Summary: This paper proposes a new proof method for strong normalization of classical natural deduction and calculi with control operators. For this purpose, we introduce a new CPS-translation, continuation and garbage passing style \((CGPS )\) translation. We show that this CGPS-translation method gives simple proofs of strong normalization of \(\lambda \mu ^{\rightarrow \wedge \vee \perp }\), which is introduced in [P. de Groote, in: Typed lambda calculi and applications. 5th international conference, TLCA 2001, Kraków, Poland, May 2–5, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2044, 182–196 (2001; Zbl 0981.03027)] by de Groote and corresponds to the classical natural deduction with disjunctions and permutative conversions.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus
Full Text: DOI
[1] David, R.; Nour, K., A short proof of the strong normalization of classical natural deduction with disjunction, J. symbolic logic, 68, 4, 1277-1288, (2003) · Zbl 1066.03056
[2] de Groote, P., A simple calculus of exception handling, (), 201-215 · Zbl 1063.68565
[3] de Groote, P., Strong normalization of classical natural deduction with disjunction, (), 182-196 · Zbl 0981.03027
[4] de Groote, P., On the strong normalisation of intuitionistic natural deduction with permutation-conversions, Inform. and comput., 178, 441-464, (2002) · Zbl 1031.03071
[5] Fujita, K., Domain-free λμ-calculus, Theor. inform. appl., 34, 6, 433-466, (2000) · Zbl 0974.68032
[6] Gørtz, I.L.; Reuss, S.; Sørensen, M.-H., Strong normalization from weak normalization by translation into the lambda-i-calculus, Higher-order symbolic comput., 16, 253-285, (2003) · Zbl 1074.68010
[7] T. Griffin, A formulae-as-types notion of control, in: 17th Annual ACM Symp. on Principles of Programming Languages, POPL’90, 1990, pp. 47-58
[8] R. Matthes, Stabilization—an alternative to double-negation translation for classical natural deduction, in: V. Stoltenberg-Hansen (Ed.), Proc. Logic Colloquium 2003, 2004 · Zbl 1102.03008
[9] Matthes, R., Non-strictly positive fixed points for classical natural deduction, Ann. pure appl. logic, 133, 205-230, (2005) · Zbl 1066.03057
[10] Nakazawa, K.; Tatsuta, M., Strong normalization proof with CPS-translation for second order classical natural deduction, J. symbolic logic, J. symbolic logic, 68, 4, 1415-1416, (2003), Corrigendum is available in: · Zbl 1058.03060
[11] C.-H.L. Ong, C.A. Stewart, A Curry-Howard foundation for functional computation with control, in: 24th Annual ACM Symp. on Principles of Programming Languages, POPL’97, 1997, pp. 215-227
[12] Parigot, M., λμ-calculus: an algorithmic interpretation of classical natural deduction, (), 190-201 · Zbl 0925.03092
[13] Parigot, M., Strong normalization for second order classical natural deduction, J. symbolic logic, 62, 4, 1461-1479, (1997) · Zbl 0941.03063
[14] Plotkin, G., Call-by-name, call-by-value and the λ-calculus, Theoret. comput. sci., 1, 125-159, (1975) · Zbl 0325.68006
[15] Yamagata, Y., Strong normalization of second order symmetric lambda-mu calculus, (), 459-467 · Zbl 1087.68538
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.