Speaker:  Paolo Di Giamberardino


Quando:  07/05/2010  11:30


Dove:  Aula Verra, FacoltÃ di Lettere e Filosofia  UniversitÃ Roma Tre, via Ostiense 234


Abstract
In previous works, by importing ideas from game semantics (notably FaggianMaurelCurien's ludics nets), we defined a new class of multiplicative/additive polarized proof nets, called Jproof nets. The distinctive feature of Jproof 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 Jproof 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 cone defined by means of jumps. As 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 partially overlapping. Moreover, we define normalization for exponential Jproof nets, proving, by Gandy's method, that even in case of ''superposed'' cones, reduction enjoys confluence and strong normalization. 