Thorsten Altenkirch

University of Nottingham

Thorsten Altenkirch is a Professor of Computer Science at the University of Nottingham known for his research on logic, type theory, and homotopy type theory. Altenkirch was part of the 2012/2013 special year on univalent foundations at the Institute for Advanced Study. At Nottingham he co-chairs the Functional Programming Laboratory with Graham Hutton.

Why Type Theory matters

Modern Type Theory (usually called Homotopy Type Theory) is at the same time the ultimate functional programming language and a novel foundation of Mathematics, an alternative to the mathematical assembly language called set theory. Type theory exploits the advantages of static typing to the limit, meaning that by hiding implementation details you can identify tow object which behave the same - this is called the univalence principle.

Video ←Back