System L syntax for sequent calculi

Pierre-Louis Curien

Programmes, Preuves et Systèmes
Université Denis Diderot (Paris 7)

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

ERDF
Tarmo Uustalu
Last update 6.12.2012