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.
The power of Π
Typed functional programming centers around the function type written → but once we allow the result type to depend on the input we obtain the dependent function type which is often written using the large greek letter Π.
I argue that in many situations in functional programming you need to use dependent types. Indeed, typed programming without dependency ignores many important constructions. On the other hand dependent types add enormous expressivity, in particular they enable us to capture gradual typing.
I will discuss applications of dependently typed programming and look into the challenges of implementing and using dependently typed languages.
Disclaimer: the title of this talk is stolen from an excellent paper by Nicolas Oury and Wouter Swierstra. While they are related in spirit they are not identical in content and Nicolas and Wouter bear no responsibility for what I am saying.
Video ←Back
