Abstract: In many programming languages, values have an associated type that the compilers enforces. For example, adding a value of type INTEGER to a value of type STRING will be flagged as an error by these compilers. Such checks by the compiler helps in eliminating a large class of bugs that arise in practice.
A proof assistant is a program that checks a formal proof for correctness. It turns out that verifying mathematical proofs are closely connected to checking types in a sufficiently sophisticated programming language. This connection goes by the name Curry-Howard isomorphism although several others have independently made the above connection. One of the goals of my talk is to give an overview of this deep connection.
Having introduced the basics of type theory, I will look at the exciting new developments in this area: the theory of homotopy types and univalent foundation.
I will try to make this talk as self contained as possible. In particular no background on programming languages, type theory or homotopy theory will be assumed.
