期刊
MATHEMATICS
卷 9, 期 4, 页码 -出版社
MDPI
DOI: 10.3390/math9040385
关键词
CPS transformation; double negation translation; simply typed lambda-calculus; propositional logic; Curry-Howard isomorphism
类别
资金
- National Research Foundation of Korea (NRF) - Korea government (MSIT) [2019R1F1A1063272, 2020R1A4A3079947]
- National Research Foundation of Korea [2019R1F1A1063272, 2020R1A4A3079947] Funding Source: Korea Institute of Science & Technology Information (KISTI), National Science & Technology Information Service (NTIS)
This paper discusses the method of embedding classical logic into intuitionistic logic using double negation translation, as well as continuation passing style transformation implemented through the Curry-Howard isomorphism in programming languages. By selectively translating nontrivial expressions into CPS functions using a type and effect system, a logical account of CBV selective CPS transformation is provided. The selective DNT derived from the corresponding type and effect system can translate classical proofs into equivalent intuitionistic proofs, presenting a smaller scale compared to traditional DNTs.
A double negation translation (DNT) embeds classical logic into intuitionistic logic. Such translations correspond to continuation passing style (CPS) transformations in programming languages via the Curry-Howard isomorphism. A selective CPS transformation uses a type and effect system to selectively translate only nontrivial expressions possibly with computational effects into CPS functions. In this paper, we review the conventional call-by-value (CBV) CPS transformation and its corresponding DNT, and provide a logical account of a CBV selective CPS transformation by defining a selective DNT via the Curry-Howard isomorphism. By using an annotated proof system derived from the corresponding type and effect system, our selective DNT translates classical proofs into equivalent intuitionistic proofs, which are smaller than those obtained by the usual DNTs. We believe that our work can serve as a reference point for further study on the Curry-Howard isomorphism between CPS transformations and DNTs.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据