首页 | 本学科首页   官方微博 | 高级检索  
     


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 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号