In a previous work, we introduced a framework for the proof nets of the multiplicative fragment of Linear Logic, where partially sequentialised nets are allowed. In this seminar we extend this result to include additives, using a definition of proof nets, called J-proof nets, which is the typed version of the L-nets of Faggian and Maurel.
In J-proof nets, we can characterize nets with different degrees of sequentiality, by gradual insertion of sequentiality constraints (jumps). As a byproduct, we obtain a simple proof of the sequentialisation theorem.