Programmes, Preuves et Systèmes
Université Denis Diderot (Paris 7)
Thursday, 6 December 2012, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: We explore (or rather revisit) a lozenge of translations from classical logic (Girard's LC or lambda-mu-calculus) to linear logic, and of corresponding model constructions, under the glasses of polarisation: these translations restrict the structural rules on positives, and then on negatives, or vice-versa. In particular, we show that the natural target is not linear logic, but Melliès' tensor logic.
(Joint work with Guillaume Munch-Maccagnoni.)
(This talk may be followed independently from the first one.)