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