University of Cambridge > Talks.cam > Trinity Mathematical Society > Dependent Type Theory

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity