Polarized and focalized linear and classical proofs

, &
Annals of Pure and Applied Logic 134 (2):217-264 (2005)
  Copy   BIBTEX

Abstract

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 and perfectly fits normalization of polarized proof-nets. Some more semantical considerations allow us to recover LC as a refinement of multiplicative

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2004.11.002

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 106,621

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Polarized games.Olivier Laurent - 2004 - Annals of Pure and Applied Logic 130 (1-3):79-123.
A categorical semantics for polarized MALL.Masahiro Hamano & Philip Scott - 2007 - Annals of Pure and Applied Logic 145 (3):276-313.
SN and CR for free-style LKtq: linear decorations and simulation of normalization.Jean-Baptiste Joinet, Harold Schellinx & Lorenzo Tortora De Falco - 2002 - Journal of Symbolic Logic 67 (1):162-196.
A phase semantics for polarized linear logic and second order conservativity.Masahiro Hamano & Ryo Takemura - 2010 - Journal of Symbolic Logic 75 (1):77-102.
Decision problems for propositional linear logic.Patrick Lincoln, John Mitchell, Andre Scedrov & Natarajan Shankar - 1992 - Annals of Pure and Applied Logic 56 (1-3):239-311.
A new deconstructive logic: Linear logic.Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx - 1997 - Journal of Symbolic Logic 62 (3):755-807.
Proof nets sequentialisation in multiplicative linear logic.Paolo Di Giamberardino & Claudia Faggian - 2008 - Annals of Pure and Applied Logic 155 (3):173-182.
Full intuitionistic linear logic.Martin Hyland & Valeria de Paiva - 1993 - Annals of Pure and Applied Logic 64 (3):273-291.
Kripke semantics and proof systems for combining intuitionistic logic and classical logic.Chuck Liang & Dale Miller - 2013 - Annals of Pure and Applied Logic 164 (2):86-111.
On the Pi-calculus and Linear Logic.Gianluigi Bellin & P. J. Scott - 1992 - LFCS, Department of Computer Science, University of Edinburgh.

Analytics

Added to PP
2013-10-30

Downloads
67 (#344,914)

6 months
10 (#387,100)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Myriam Quatrini
Aix-Marseille University

Citations of this work

A focused approach to combining logics.Chuck Liang & Dale Miller - 2011 - Annals of Pure and Applied Logic 162 (9):679-697.
Linear logic.Roberto Di Cosmo & Dale Miller - unknown - Stanford Encyclopedia of Philosophy.

Add more citations

References found in this work

Proofs and types.Jean-Yves Girard - 1989 - New York: Cambridge University Press.
Linear Logic.Jean-Yves Girard - 1987 - Theoretical Computer Science 50:1–101.
The additive multiboxes.Lorenzo Tortora de Falco - 2003 - Annals of Pure and Applied Logic 120 (1-3):65-102.

View all 6 references / Add more references