#### 2011

#### Paolo Di Giamberardino

#### Mathematical Structures in Computer Science, special issue on `DIFFERENTIAL LINEAR LOGIC, NETS, AND OTHER QUANTITATIVE AND PARALLEL APPROACHES TO PROOF-THEORY''

#### Abstract

In previous works, by importing ideas from game semantics (notably

Faggian-Maurel-Curien's \emph{ludics nets}), we defined a new class of

multiplicative/additive polarized proof nets, called \emph{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 \emph{jumps} (that is, untyped extra edges) as

sequentiality constraints. Starting from this result, in the present work we

extend J-proof nets to the multiplicative/exponential fragment, in order to take into account structural rules: more precisely, we

replace the familiar linear logic notion of exponential box with a less restricting one (called \emph{cone})

defined by means of jumps. As a consequence, we get a syntax for

polarized nets where, instead of a structure of boxes nested one into the other,

we have one of cones which can be \emph{partially overlapping}. Moreover, we define cut-elimination for exponential J-proof nets, proving, by a variant of Gandy's method, that even in case of ``superposed'' cones, reduction enjoys confluence and strong

normalization.

#### Download: JumpExponentials.pdf

**BibTeX**