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.
