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.