Date:
Wednesday, 12 March, 2025 - 17:00 to 18:00
Speaker:
Francisco Ferreira Ruiz (Royal Holloway, University of London)
Venue:
MR14 Centre for Mathematical Sciences
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
NOTE UNUSUAL DAY
Seminar series:
Formalisation of mathematics with interactive theorem provers
