On Correspondence between Selective CPS Transformation and Selective Double Negation Translation

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.

Automated summary

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.