Research

The Tao of Types

Location
B52, Business School South, Jubilee Campus
Date(s)
20/11/2019 (17:30-19:30)
Contact
Clair Morton clair.morton@nottingham.ac.uk
Registration URL
https://tao-of-types-2019.eventbrite.co.uk/
Description
416998-INAUGURAL-ResearchEventHeader-735x300px-CMG-OCT19

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.

World-class research at the University of Nottingham

University Park
Nottingham
NG7 2RD
+44 (0) 115 951 5151
research@nottingham.ac.uk
Athena Swan Logo