# ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

# Logic in Computer Science (LICS 2003)

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

Authors: 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}
}