Computerphile
The Hardest Problem in Type Theory
2021 • E29 Jul 30, 2021 24m
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.