Programming and Proving in Homotopy Type Theory
In this talk, I will describe my work on Homotopy Type Theory, which is a new foundation for proof assistants. Homotopy Type Theory extends type theory, the basis of several successful proof assistants, with new principles that bring it closer to informal mathematical practice. Moreover, it is based on an exciting new correspondence between type theory and the mathematical disciplines of homotopy theory and category theory, and consequently can be used to directly describe structures in these areas of math. I will describe computer-checked proofs of some basic results in algebraic topology, including calculations of homotopy groups of spheres and Eilenberg-MacLane spaces. Homotopy Type Theory is also a programming language, in which the new mathematical principles correspond to new programming techniques, which make certain programs easier to write. I will also describe my work on using Homotopy Type Theory as a programming language and its applications in computer science.
Dan Licata received his PhD from Carnegie Mellon University in 2011, advised by Robert Harper. His dissertation, Dependently Typed Programming with Domain-Specific Logics, won the FoLLI E.W. Beth Dissertation Award in 2012. After graduating, he spent three semesters as a teaching fellow at Carnegie Mellon, designing and delivering a new introductory course on functional programming, parallelism, and verification. This year, he is a post-doctoral member at the Institute for Advanced Study, which is hosting a year-long program on an exciting new connection between programming languages and mathematics. His research focuses on creating better tools for computer-checked mathematics and software verification.