BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Dependent Type Theory - Will Sonnex (Computer Lab)
DTSTART:20140223T150000Z
DTEND:20140223T153000Z
UID:TALK50871@talks.cam.ac.uk
CONTACT:Mary Fortune
DESCRIPTION:What is a mathematical proof as a mathematical object? How do 
 we axiomatize mathematics so that computers can check our proofs\, or cons
 truct their own (my research)? This talk answers these questions using Dep
 endent Type Theory\, and I will show how complex modern mathematics can be
  built out of this simple starting language (all checked by a computer too
 ). At the end I will discuss some of the exciting recent developments in H
 omotopy Type Theory.
LOCATION:Winstanley Lecture Theatre\, Trinity College
END:VEVENT
END:VCALENDAR