Séminaire, 12 mars 2015

Programme

10:30 – 12:00

Thomas Ehrhard (CNRS, Univ. Paris Diderot)

Invited talk: Un critère de correction de Christian Rétoré

14:00 – 15:00

Amina Doumane (Université Paris Diderot and ENS Cachan)

Invited talk: On the dependencies of logical rules

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)

Invited talk: Injectivity of relational semantics for connected MELL proof-structures via Taylor expansion

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.