Seminari del Dipartimento
Logica Matematica Coends and proof equivalence in second order multiplicative linear logic Paolo Pistone 21-12-2018 - 16:00 Largo San Leonardo Murialdo,1 - Pal.C - Aula 311 - III piano
Proof nets for multiplicative linear logic (MLL) provide canonical representations of proofs: they are permutation-independent, separable and are injectively interpreted in the relational and coherent semantics. None of these properties scales to second order multiplicative linear logic (MLL2): proof nets for MLL2 are not invariant with respect to all valid permutations, are not separable and are not injectively interpreted in either the relational or coherent semantics. This problem is related to the interpretation of the existential quantifier. In categorical terms this should correspond to a coend, a special colimit defined in terms of dinatural transformations. However, usual proof nets violate the diagrams defining a coend. Starting from this intuition, we investigate the problem of defining canonical proof nets for MLL2 as a coherence problem for coends over a compact-closed category and we show some results concerning some fragments of MLL2. |