BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The direct approach to evaluation order - Guillaume Munch-Maccagno
 ni\, INRIA
DTSTART:20180619T130000Z
DTEND:20180619T140000Z
UID:TALK106576@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:This talk is about the theory of computation with evaluation o
 rder\, for instance in the presence of effects and/or resources. I will re
 visit the relationship between two lines of work in this context: focusing
  (from the proof search paradigm) and call-by-push-value (from the monadic
  semantics paradigm). I present a self-contained approach which contains\,
  connects\, and generalizes their principal concepts and results. Both par
 adigms gain new questions\, and their relationship is explained\, as they 
 become unified. The result is a Curry-Howard correspondence in the origina
 l sense of Lambek: an internal language for call-by-push-value that comes 
 with a guarantee of fitness for a purpose\, here for instance we obtain fo
 r free a solution to the word problem. As for the old formalisms\, some ar
 e decomposed (focusing)\, others are made redundant (call-by-push-value-st
 yle syntaxes).\n\nThe approach is built on top of an old theorem due to F
 ührmann relating “direct-style” deductive systems to algebraic models
 . Until recently this result was more of a curiosity\, but it has resurfac
 ed in several works. I propose to make it a mediating principle between lo
 gic\, computation and algebra\, so the talk will focus on explaining this 
 point of view.
LOCATION:FW26
END:VEVENT
END:VCALENDAR