seminaire PPS Jeudi 15/4

Chers tous,
prochaine seminaire PPS:

Jeudi 15 Avril, 11h salle 3E91

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.