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

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Dependent Type Theory

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 ex-directory lists are not shown.

Other lists

Webinar (via Zoom online). GS1 Faculty of Education, Donald McIntyre Building Faculty of Education, Donald McIntyre Building, 184 Hills Road CB2 8PQ, Room 1S3 DMB

Other talks

Title TBC Claudia Ribeiro Almeida, Group Leader, Babraham Institute Title TBC Shining a light on the origin of supermassive black holes with cosmological simulations Online Causal Inference Seminar Title to be confirmed
 

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