Dependent Type Theory
Add to your list(s)
Download to your calendar using vCal
If you have a question about this talk, please contact Mary Fortune.
Part of the TMS Symposium
What is a mathematical proof as a mathematical object? How do we axiomatize mathematics so that computers can check our proofs, or construct their own (my research)? This talk answers these questions using Dependent Type Theory, and I will show how complex modern mathematics can be built out of this simple starting language (all checked by a computer too). At the end I will discuss some of the exciting recent developments in Homotopy Type Theory.
This talk is part of the Trinity Mathematical Society series.
This talk is included in these lists:
Note that exdirectory lists are not shown.
