The inaugural lecture of the Tao of Types presented by professor Thorsten Altenkirch

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 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 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.

This lecture will take place between 6-7pm on Wednesday 20 November in B52, Business School South on Jubilee Campus.

Light refreshments will be available in the foyer before the lecture from 5.30pm. A drinks reception will follow the lecture between 7pm and 7.30pm.

This event is free to attend and booking is required.

For more information, and to book your place, please visit the event page.