Speaker: Professor Thorsten Altenkirch, School of Computer Science, Faculty of Science
Types play an important role in computer science and mathematics, they are an alternative to the ubiquitous sets. Types provide a disciplined approach to organising software and mathematical constructions and via the propositions as types translation they provide an alternative to the classical approach to logic. We will give an overview over the evolving field of Type Theory, which is the basis of systems for computer aided formal reasoning like Coq and Agda, but is also provides a different way to think about programs and proofs. We will also cover the latest development, Homotopy Type Theory, which creates a surprising connection between very abstract geometry (Homotopy Theory) and types.
Thorsten Altenkirch is from Berlin and worked as a programmer there for various companies. It was there he got sucked into more theoretical realms doing a PhD on Type Theory. Following this ambition he has been working in Gothenburg and Munich. Eventually at the turn of the Millenium, Thorsten joined the School for Computer Science at the University of Nottingham, where he founded the Functional Programming Laboratory together with his colleague Graham Hutton.