Sciweavers

Share
LICS
2003
IEEE

About Translations of Classical Logic into Polarized Linear Logic

9 years 5 months ago
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.
Olivier Laurent, Laurent Regnier
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where LICS
Authors Olivier Laurent, Laurent Regnier
Comments (0)
books