Richard Garner
Macquarie University

"Homotopy type theory"

Homotopy type theory is a fascinating new area of research which sits
at the intersection of algebraic topology and type theory; the big
surprise being that this intersection is non-empty. More precisely,
what has come to light over the past few years is that Martin-Löf type
theory---the system underlying proof assistants like Coq and
Agda---can be used for directly formalising arguments from algebraic
topology, and so for calculating fundamental invariants of geometric
objects. The arguments used are a curious mixture of very classical
mathematics and very modern dependently-typed programming. This talk
will attempt to give a brief flavour of what is involved.