- About Translations of Classical Logic into Polarized Linear Logic doi link

Auteur(s): Laurent Olivier, Regnier Laurent

Conference: (, , 2003)
Actes de conférence: Logic in Computer Science, vol. p.11-20 (2003)

Ref HAL: hal-00009139_v1
DOI: 10.1109/LICS.2003.1210040
Exporter : BibTex | endNote

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