Cancelled for 30 May 2012: to be rescheduled

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.

Cancelled for today: to be rescheduled

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.

Cancelled for today: to be rescheduled

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.

Cancelled for today: to be rescheduled

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.

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.