BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Selection functions everywhere - MartÃn EscardÃ³\,
University of Birmingham
DTSTART;TZID=Europe/London:20110128T140000
DTEND;TZID=Europe/London:20110128T150000
UID:TALK29364AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/29364
DESCRIPTION:I'll present the theory of selection functions\, w
ith applications to game theory\, proof theory and
topology\, among others.\n\nSelection functions f
orm a strong monad\, which can be defined in any c
artesian closed category\, and has a morphism into
the continuation monad. In certain categories of
spaces and domains\, the strength can be infinitel
y iterated. This infinite strength is an amazingly
versatile functional that (i) optimally plays seq
uential games\, (ii) realizes the Double Negation
Shift used to realize the classical axiom of count
able choice\, and (iii) implements a computational
version of the Tychonoff Theorem from topology. T
he infinite strength turns out to be built-in in t
he functional language Haskell\, called sequence\,
and can be used to write unexpected programs that
compute with infinite objects\, sometimes surpris
ingly fast. The selection monad also gives rise to
a new translation of classical logic into intuiti
onistic logic\, which we refer to as the Peirce tr
anslation\, as monad algebras are objects that sat
isfy Peirce's Law.\n\nThis is joint work with Paul
o Oliva from Queen Mary.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Bu
ilding
CONTACT:Bjarki Holm
END:VEVENT
END:VCALENDAR