BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:What can sequent calculus do for functional programs? - Pierre-Lou
 is Curien\, Paris
DTSTART:20090617T131500Z
DTEND:20090617T141500Z
UID:TALK18723@talks.cam.ac.uk
CONTACT:Mateja Jamnik
DESCRIPTION:(in memory of Peter Landin (1930-2009)  and Gerhard Gentzen (1
 909-1945))\n\nGentzen is at the origin of natural deduction and sequent ca
 lculus.  \nBoth had a deep echo in computer science\, the first via the Cu
 rry- \nHoward correspondence linking\nlambda-calculus based programming la
 nguages with formal proofs  \nwritten in natural deduction style\, while t
 he second led to the proof- \nsearch paradigm at the heart of logic progra
 mming.  In this talk\, we  \nshall start from the backbone of Curry-Howard
 \, which is simply typed  \nlambda-calculus on one side\, intuitionistic l
 ogic on the other side\, and\nexplain a few milestones:\n\n* Griffin  1990
 : extending the picture to control operators on one  \nside\, classical lo
 gic on the other side\n* Herbelin 1995:  Curry-Howard in  sequent calculus
  style\n* Curien-Herbelin 2000: call-by-value is dual to call-by-name\n* M
 unch\, Curien-Munch 2008: focalised Curry-Howard\, where the order  \nof e
 valuation is reflected at the level of types/formulas  (see also  \nZeilbe
 rger 2008)\n\nIn a nutshell\, the sequent calculus offers symmetries betwe
 en inputs  \nand continuations\, and between\nprograms and program context
 s\, that make sequent calculus based  \nsyntaxes suitable for the formalis
 ation of abstract machines.\n\n(Supported by Leverhulme grant)
LOCATION:Lecture Theatre 1\, Computer Laboratory
END:VEVENT
END:VCALENDAR