Autori: Maieli, Roberto; Abrusci, Vito Michele

Editore: Cambridge University Press

Tipologia Prodotto: Articolo in rivista

DOI: 10.1017/S0960129518000300

Titolo della Rivista: MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE

Numero;Volume: 6; 29

Numero prima e ultima pagina: 733 – 762

Codice ISSN/ISBN/ISMN: 0960-1295 (Stampa) , 1469-8072 (Online)

Anno di Pubblicazione: 2019

Abstract:

This paper presents a simple and intuitive syntax for proof nets of the multiplicative cyclic fragment (McyLL) of linear logic (LL). The main technical achievement of this work is to propose a correctness criterion that allows for sequentialization (recovering a proof from a proof net) for all McyLL proof nets, including those containing cut links. This is achieved by adapting the idea of contractibility (originally introduced by Danos to give a quadratic time procedure for proof nets correctness) to cyclic linear logic. This paper also gives a characterization of McyLL proof nets for Lambek Calculus and thus a geometrical (i.e., non inductive) way to parse phrases or sentences by means of Lambek proof nets.