About translations of classical logic into polarized linear logic

摘要

We show that the decomposition of intuitionistic logic into linear logic along the equation A /spl rarr/ B = !A /spl rarr/ B may be adapted into a decomposition of classical logic into LLP, the polarized version of Linear Logic. Firstly, we build a categorical model of classical logic (a control category) from a categorical model of linear logic by a construction similar to the co-Kleisli category. Secondly, we analyze two standard continuation-passing style (CPS) translations, the Plotkin and the Krivine's translations, which are shown to correspond to two embeddings of LLP into LL.