BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Lab Lunch
SUMMARY:A continuous computational interpretation of type
theories - Chuangjie Xu (University of Birmingham)
DTSTART:20150309T120000Z
DTEND:20150309T130000Z
UID:TALK1712AT
URL:/talk/index/1712
DESCRIPTION:We develop a constructive variation of Johnstone's
topological topos to \nprovide a computational in
terpretation of type theory validating \nBrouwer’s
uniform-continuity principle\, so that type-theor
etic proofs \nwith the principle as an assumption
have computational content. The \nconstruction of
our model and the verification of the uniform-con
tinuity \nprinciple have been formalized in intens
ional Martin-Löf type theory in \nAgda notation.
Hence we obtain a program of computing least modul
i of \nuniform continuity!\n
LOCATION:CS 217
CONTACT:Uday Reddy
END:VEVENT
END:VCALENDAR