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 Symp. on Logic in Computer Science, {LICS} 2003},
year =	 2003,
editor =	 {Phokion G. Kolaitis},
month =	 {June},
pages =      {11--20},