The Hardest Problem in Type Theory – Computerphile

Equality sounds a straightforward idea, but there are subtle problems in theoretical computer science. Professor Thorsten Altenkirch explains how his late friend Martin Hofmann solved one of the biggest problems.

More of Thorsten on Type Theory:

Thorsten’s paper dedicated to Martin:

This video was filmed and edited by Sean Riley.

Computer Science at the University of Nottingham:

Computerphile is a sister project to Brady Haran’s Numberphile. More at

Leave a comment

Your email address will not be published. Required fields are marked *