University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Why do I write proofs?

  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

Why do I write proofs?

Download to your calendar using vCal

If you have a question about this talk, please contact Anand Rao Tadipatri .

NOTE UNUSUAL DAY

In this talk I explore the purpose of mechanised proofs in my research in programming languages. I do not think that my reasons are very personal or specific, so I hope the reasons are of interest to others. I will talk about three scenarios. The first illustrates how proofs clarify existing ideas. Then, how certified tools can be built from formalised proofs. And finally proofs serve as an exploratory tool to develop new ideas on a solid foundation.

=== Hybrid talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1

Meeting ID: 871 4336 5195

Passcode: 541180

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Room GS15 at the William Gates Building and on Zoom: https://cl-cam-ac-uk.zoom.us/j/4361570789?pwd=Nkl2T3ZLaTZwRm05bzRTOUUxY3Q4QT09&from=addon Join Zoom Meeting https://zoom.us/j/94056313546?pwd=N1dYVFR1b0FwNmk0eGlxeDd1OVY1QT09 Meeting ID: 940 5631 3546 Passcode: 313690 SCR, Dept. of Veterinary Medicine

Other talks

What Can a Spectrum Learn? AI Perspectives on the Kohn Laplacian of Sphere Quotients Group Presentation 4 Coming soon Title to be confirmed Not-so-noble gases, key tracers of Earth’s habitability: what their behaviour in planetary interiors can tell us? Quantum optics with organic molecules
 

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