This talk examines one of the idiosyncrasies of dependently typed programming, the requirement for totality. We will see why we have this requirement and how the current approach to satisfying this requirement is distinctly unpalatable for programmers.
Donovan will introduce the main thrust of his research, namely using a type-theoretic approach to ensuring totality and outline the steps needed to take this idea to a working implementation.
Along the way, we will (briefly) examine concepts such as: dependent types, type theories, extensionality, intensionality, induction, co-induction, formalisation or mechanisation, and semantics.