## Paper: About Translations of Classical Logic into Polarized Linear Logic (at LICS 2003)

**Olivier Laurent Laurent Regnier**

### Abstract

We show that the decomposition of Intuitionistic Logic into Linear Logic along the equation A \rightarrow B = !A \multimap 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 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.

### BibTeX

@InProceedings{LaurentRegnier-AboutTranslationsof, author = {Olivier Laurent and Laurent Regnier}, title = {About Translations of Classical Logic into Polarized Linear Logic}, booktitle = {Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003)}, year = {2003}, month = {June}, pages = {11--20}, location = {Ottawa, Canada}, publisher = {IEEE Computer Society Press} }