BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Polarisation in classical realisability and delimited control - Gu
 illaume Munch-Maccagnoni
DTSTART:20110614T114500Z
DTEND:20110614T130000Z
UID:TALK31761@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:In the quest of a proofs-as-programs interpretation of real-wo
 rld mathematics\, surely the big scale is interesting (for instance axioms
  with involved computational content such as dependent choice) but the sma
 ll scale is equally important (operational details inspired by CPS and lin
 ear logic semantics\, such as polarities).\n\nOne striking polarity-relate
 d phenomenon is the duality between the call-by-value and the call-by-name
  evaluation paradigms in the presence of call/cc-like control operators. C
 urien and Herbelin (2000) captured this phenomenon in an elegant way with 
 a symmetric syntax\nthat could express the symmetries of sequent calculus.
   I will argue that this result is more than a beautiful curiosity ---  it
  also provides us with a new tool for investigating the proofs-as-programs
  correspondence in a unified fashion.\n\nFirst I would like to explain the
  path from lambda calculus to Girard's polarised classical logic using ste
 pping stones from the semantics of programming languages (Moggi's monadic 
 calculus\, duality between call-by-name and call-by-value\, call-by-push-v
 alue).\n\nThen I would like to sketch in a nutshell how a polarised varian
 t of Curien-Herbelin's notation can help to show\n\n* the importance of ph
 enomena linked to polarisation in Krivine's classical realisability\, and\
 n\n* how polarisation can help answer the question "what is a call-by-name
  counterpart to Danvy-Filinski's delimited control calculus?". (Confirming
  results from my last year's work-in-progress talk)\n\n
LOCATION:Room SS03\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR