Tuesday, 4 December 2012, 11:00 (note the unusual weekday and time)
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: We present a style of syntax for sequent calculus (whence the name "system L") proofs, inspired by the syntax of Curien and Herbelin (lambda-bar-mu-mu-tilde calculus) that was originally designed twelve years ago to express the duality of call-by-name and call-by-value, and to give a first-class logical status to abstract machine states. The current formulation takes full profit of polarisation and focalisation, that are now better understood. It unifies a number of calculi and logics present in the literature, including Girard's LC, Laurent's LLP, Melliès' tensor logic, Levy's CBPV...
(Joint work with Guillaume Munch-Maccagnoni.)