BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:From Brouwer's Thesis to the Fan Functional - Ulri
ch Berger (Swansea University)
DTSTART:20200221T110000Z
DTEND:20200221T120000Z
UID:TALK4173AT
URL:/talk/index/4173
DESCRIPTION:The usual formulation of Brouwer's Thesis ('every
bar is inductive')\nuses quantification over infin
ite sequences of natural numbers to\ndefine what a
bar is. We propose an alternative formulation th
at\navoids infinite sequences and instead uses a c
oinductive definition to\nexpress the bar property
. This coinductive formulation leads to a\n(new?)
abstract version of Bar Induction which\, combine
d with a\nmodality for trivial truth\, makes it po
ssible to prove constructively\nthat every continu
ous fuction on Cantor space is uniformly\ncontinuo
us. The computational content of that proof is a p
urely\nfunctional implementation of Tait's Fan Fun
ctional computing the\nminimal modulus of uniform
continuity of such functions.
LOCATION:Computer Science\, The Sloman Lounge (UG)
CONTACT:Vincent Rahli
END:VEVENT
END:VCALENDAR