Séminaire, March 12, 2015


10:30 – 12:00
Thomas Ehrhard (CNRS, Univ. Paris Diderot)
14:00 – 15:00
Amina Doumane (Université Paris Diderot and ENS Cachan)

Many correctness criteria have been proposed since linear logic was introduced and it is not clear how they relate to each other. We present proof-nets and their correctness criteria from the perspective of dependency, as introduced by Mogbil and Jacobé de Naurois.

More precisely, we introduce a new correctness criterion, called DepGraph, and show that together with Danos' contractibility criterion and Mogbil and Naurois criterion, they form the three faces of a notion of dependency which is crucial for correctness of proof-structures.

Finally, we extract the logical meaning of the dependency relation and show that it allows to recover and characterize some constraints on the ordering of inferences which are implicit in the proof-net.

15:30 – 16:30
Giulio Guerrieri (Université Paris Diderot)

We show that:

(1) the Taylor expansion of a cut-free MELL proof-structure R with atomic axioms is the (most informative part of the) relational semantics of R;

(2) every box-connected MELL proof-structure is uniquely determined by the element of order 2 of its Taylor expansion;

(3) the relational semantics is injective for box-connected MELL proof-structures.

We point out that our notion of box-connection is rather general: all ACC or connected proof-structures are box-connected (the converse does not hold).

This is joint work with Lorenzo Tortora de Falco. Our results are deeply related to a previous work of Lorenzo Tortora de Falco and Daniel de Carvalho, but is based on a slightly different viewpoint.