Why do I write proofs?

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

• Francisco Ferreira Ruiz (Royal Holloway, University of London)
• Wednesday 12 March 2025, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

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:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.