Paolo Di Giamberardino (LIPN, Paris)

Jump from parallel to sequential proofs: exponentials.

In previous works, by importing ideas from game semantics (notably Faggian-Maurel-Curien's ludics nets), we defined a new class of multiplicative/additive polarized proof nets, called J-proof nets. The distinctive feature of J-proof nets with respect to other proof net syntaxes, is the possibility of representing proof nets which are partially sequentialized, by using jumps (that is, untyped extra edges) as sequentiality constraints. Starting from this result, in the present work we extend J-proof nets to take into account structural rules: more precisely, we show that in J-proof nets the familiar linear logic notion of exponential box could be represented by means of jumps. As consequence, we get a syntax for polarized nets where the usual nesting condition on exponential boxes is relaxed, allowing a partial superposition of boxes. Moreover, we prove that, even in case of ''superposed'' boxes, reduction enjoys confluence and strong normalization, using Gandy's method.