Warning: Table './church/sessions' is marked as crashed and last (automatic?) repair failed query: SELECT sid FROM sessions WHERE sid = 'srmi5a1c85qppagtaotn7isj93' in /var/www/church/includes/database.mysql.inc on line 121
Jump from Parallel to Sequential Proofs: Additives. | Gruppo di Logica e Geometria della Cognizione

Jump from Parallel to Sequential Proofs: Additives.

2011

Paolo Di Giamberardino

Université Paris 13

Technical report (Rapport Interne LIPN)

Abstract

In previous work, we introduced a framework for proof nets of the multiplicative fragment of Linear Logic, where \emph{partially sequentialized} nets are allowed.

In this paper we extend this result to include additives, using a definition of proof net, called \emph{J-proof net}, which corresponds to a typed version of an L-net of Faggian and Maurel.

In J-proof nets, sequentiality constraints are represented using the proof-net notion of \emph{jumps}; by gradual insertion or removal of jumps then it is possible to characterize nets with different degrees of sequentiality. As a byproduct, we obtain then a proof of the sequentialization theorem.

Moreover, we provide a denotational model for J-proof nets which is an extension of the relational one, and we show that the ``degree'' of sequentiality of a J-proof net can be read-off from its semantics, by proving that the model is injective with respect to J-proof nets.

Download: jumpsadditive.pdf

BibTeX


Warning: Can't find file: 'watchdog' (errno: 2) query: INSERT INTO watchdog (uid, type, message, severity, link, location, referer, hostname, timestamp) VALUES (0, 'php', 'Table './church/sessions' is marked as crashed and last (automatic?) repair failed\nquery: SELECT sid FROM sessions WHERE sid = 'srmi5a1c85qppagtaotn7isj93' in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/node/156', '', '44.220.251.236', 1728501990) in /var/www/church/includes/database.mysql.inc on line 121