Jump from Parallel to Sequential Proofs: Additives.


Paolo Di Giamberardino

Université Paris 13

Technical report (Rapport Interne LIPN)


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