A classical lozenge

Pierre-Louis Curien

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.)

Tarmo Uustalu
Last update 6.12.2012