About Translations of Classical Logic into Polarized Linear Logic

We show that the decomposition of Intuitionistic Logic into Linear Logic along the equation ´ 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 analyse 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.

• Type: Conference
• Year: 2003
• Where: LICS
• Authors: Olivier Laurent, Laurent Regnier
• Keywords: Categorical Model, Classical Logic, Computer Science, LICS 2003, Linear Logic