Loïc Pujet: An intro to computer-assisted proofs with Coq
Tid: On 2023-11-15 kl 13.30 - 14.30
Plats: Cramer room, Albano
Medverkande: Loïc Pujet (SU)
Abstract
Proof assistants are software programs that help you in elaborating proofs for mathematical theorems and certified programs, and in making sure that you did not miss a step in your reasoning. Over the last few years, these systems have been trying to make their way into the working mathematician's toolbox.
In this talk, I will introduce Coq, a modern proof assistant based on dependent type theory. I will show different ways of using it, to write both certified programs and mathematical proofs. If time permits, I will briefly discuss the logical foundations of proof assistants.