Homotopy type theory at IITK

Steve Awodey is going to talk about homotopy type theory at our department on 14th of January, 2015 at 3:00pm. This will be the 6th Hari V Sahasrabuddhe Inflections in Computing lecture. The abstract is given below.

Homotopy type theory is a homotopical interpretation of a system of constructive type theory. It provides a new framework for the foundations of mathematics with intrinsic geometric content and a computational implementation. It is currently under intense development by logicians, mathematicians and computer scientists as a potential tool for both the large-scale formalization and verification of mathematical proofs and formal verification of software. In this survey talk, I will introduce this system and show how it can be used to give new logical proofs of some classical theorems from algebraic topology, making use of the new ideas of higher inductive types and the univalence axiom.

For information, see http://www.homotopytypetheory.org.