Dependent Type Theory

Add to your list(s) Download to your calendar using vCal

• Will Sonnex (Computer Lab)
• Sunday 23 February 2014, 15:00-15:30
• Winstanley Lecture Theatre, Trinity College.

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:

• Guy Emerson's list
• Trinity Mathematical Society
• Winstanley Lecture Theatre, Trinity College
• bld31

Note that ex-directory lists are not shown.