BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Selection functions everywhere - Martín Escardó\, University of 
 Birmingham
DTSTART:20110128T140000Z
DTEND:20110128T150000Z
UID:TALK29364@talks.cam.ac.uk
CONTACT:Bjarki Holm
DESCRIPTION:I'll present the theory of selection functions\, with applicat
 ions to game theory\, proof theory and topology\, among others.\n\nSelecti
 on functions form a strong monad\, which can be defined in any cartesian c
 losed category\, and has a morphism into the continuation monad. In certai
 n categories of spaces and domains\, the strength can be infinitely iterat
 ed. This infinite strength is an amazingly versatile functional that (i) o
 ptimally plays sequential games\, (ii) realizes the Double Negation Shift 
 used to realize the classical axiom of countable choice\, and (iii) implem
 ents a computational version of the Tychonoff Theorem from topology. The i
 nfinite strength turns out to be built-in in the functional language Haske
 ll\, called sequence\, and can be used to write unexpected programs that c
 ompute with infinite objects\, sometimes surprisingly 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 translation\, as monad alg
 ebras are objects that satisfy Peirce's Law.\n\nThis is joint work with Pa
 ulo Oliva from Queen Mary. 
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR