BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Small Proofs - Dan Licata (Wesleyan University)
DTSTART:20170711T133000Z
DTEND:20170711T143000Z
UID:TALK73233@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:There is an old idea in programming languages that the right w
 ay to solve a problem is to (1) design and implement a programming languag
 e in which solving the problem is easy\, and then (2) write the program in
  that language.  Some applications of homotopy type theory to the formaliz
 ation of mathematics have this flavor: First\, we design a type theory and
  study its semantics.  Then\, we use that type theory\, including features
  such as the univalence axiom\, higher inductives types\, interval objects
 \, and modalities\, as a language where it is easy to talk about certain m
 athematical structures\, which enables short formalizations of some theore
 ms.  In this talk\, I will give a flavor for what this looks like\, using 
 examples drawn from homotopy\, cubical\, and cohesive type theories.  I ho
 pe to stimulate a discussion about the pros and cons of factoring the form
 alization of mathematics through the design of new programming languages/l
 ogical systems.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR