loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
18th Annual IEEE Symposium on Logic in Computer Science (LICS'03)
About Translations of Classical Logic into Polarized Linear Logic
Ottawa, Canada
June 22-June 25
ISBN: 0-7695-1884-2
Olivier Laurent, Preuves Programmes Syst?mes
Laurent Regnier, Institut de Math?matiques de Luminy
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.
Citation:
Olivier Laurent, Laurent Regnier, "About Translations of Classical Logic into Polarized Linear Logic," lics, pp.11, 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.