Inaugural Lecture - Prof Thorsten Altenkirch

Inaugural Lecture - Prof Thorsten Altenkirch

The Tao of Types

Types play an important role in Computer Science and Mathematics, indeed they are an alternative to the ubiquitous sets. Types provide a disciplined approach to organizing 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 it 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 is from Berlin, Germany and has grown up on the western side of the wall. Indeed it is a little known fact that the wall was only built for him and it was taken down 6 weeks after he left to start his PhD in Edinburgh, Scotland. Having worked as a programmer in Berlin for various companies, Thorsten got sucked into more theoretical realms doing a PhD on Type Theory. Following this ambition he has been working in Gothenburg, Sweden and even in (for a Prussian from Berlin) more exotic places like Munich in catholic Bavaria. 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.

Programme

5.30pm Tea & Coffee - Foyer

6.00pm - 7.00pm Lecture - B52

7.00pm Drinks & Nibbles - Foyer

The University of Nottingham is committed to protecting your personal data and informing you of your rights in relation to that data. You can read our full privacy notice online here.