<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: arial,helvetica,sans-serif; font-size: 12pt; color: #000000'><b>Programming and Proving in Homotopy Type Theory</b>
<br>
<b><a href="http://www.cs.cmu.edu/%7Edrl/">Daniel Licata</a></b>, <a href="http://www.ias.edu/">Carnegie Mellon University & Institute for Advanced Study</a>
<br>Monday, March 25, 2013, 4:30pm<br>Computer Science 105<br>
<br>
There is a strong correspondence between mathematics and programming,
under which mathematical proofs correspond to programs. A _proof
assistant_ is a tool that a mathematician/programmer can use to
represent proofs/programs, in such a way that a computer can verify
whether or not they are correct. The use of proof assistants in math
and computer science is becoming ever more important for managing the
increasing complexity of proofs and programs. Proof assistants have
been used to check significant mathematical theorems, such as the Four
Color Theorem and the Feit-Thompson Odd-Order Theorem, as well as large
pieces of software, such as a C compiler and the definition of the
Standard ML programming language.<br><br><p>
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. <br></p><p><br></p>
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.
<br><div><span name="x"></span><br><br><br><span name="x"></span><br></div><br></div></body></html>