Polarized and focalized linear and classical proofs

We give the precise correspondence between polarized linear logic and polarized classical logic. The properties of focalization and reversion of linear proofs are at the heart of our analysis: we show that the tq-protocol of normalization for the classical systems LK pol and LK, pol perfectly fits normalization of polarized proof-nets. Some more semantical considerations allow to recover LC as a refinement of multiplicative LK pol. MSC: 03F05; 03F07; 03F52

• Type: Journal
• Year: 2005
• Where: APAL
• Authors: Olivier Laurent, Myriam Quatrini, Lorenzo Tortora de Falco
• Keywords: APAL 2005, Multiplicative Lk Pol, Polarized, Precise Correspondence