University of Cambridge > Talks.cam > Trinity Mathematical Society > Dependent Type Theory - Proving Theorems by Writing Programs

  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 - Proving Theorems by Writing Programs

Download to your calendar using vCal

If you have a question about this talk, please contact Mary Fortune .

Part of the TMS Symposium

A quick tutorial about writing programs in Agda, a language with dependently typed values. In Agda we can write a program, and then a mathematical proof that the program behaves correctly, in exactly the same language, through the magic of dependent types.

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

Room B3, Institute of Criminology St. Lukes Church, Victoria Road, Cambridge CB4 3DZ in person & via zoom

Other talks

Seminars in Cancer Title to be confirmed TBC FILM: One With The Whale Afternoon Break Title to be confirmed
 

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