Strong normalization proofs by CPS-translations |
| |
Authors: | Satoshi Ikeda Koji Nakazawa |
| |
Affiliation: | Graduate School of Informatics, Kyoto University, Yoshida-Honmachi, Sakyo-ku, Kyoto 606-8501, Japan |
| |
Abstract: | ![]() 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 λμ→∧∨⊥, which is introduced in [P. de Groote, Strong normalization of classical natural deduction with disjunction, in: S. Abramsky (Ed.), Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, in: Lecture Notes in Comput. Sci., vol. 2044, Springer, Berlin, 2001, pp. 182-196] by de Groote and corresponds to the classical natural deduction with disjunctions and permutative conversions. |
| |
Keywords: | Programming calculi Continuation passing style translation Strong normalization Classical natural deduction Permutative conversion |
本文献已被 ScienceDirect 等数据库收录! |
|