Rescheduled for 6 June 2012 at 11h (bocal, LIX)
Proof nets and semi-star-autonomous categories
Willem Heijltjes, postdoc in Parsifal
Girard’s original proof nets are a canonical graphical presentation of proof in multiplicative linear logic without units. In capturing their categorical semantics, there is the problem of dealing with proof nets that have a single conclusion. These would normally be captured by morphisms out of the monoidal unit 1; however, for MLL /with/ units, proof nets are not canonical for the semantics of star-autonomous categories. We address this issue via a set-valued functor called the /virtual unit/, that takes the place of hom(1,-). Then proof nets are canonical for a notion of semi-star-autonomous category incorporating this functor. This is joint work with Lutz Strassburger.
