Skip to main content
To KTH's start page To KTH's start page

Loïc Pujet: An intro to computer-assisted proofs with Coq

Time: Wed 2023-11-15 13.30 - 14.30

Location: Cramer room, Albano

Participating: Loïc Pujet (SU)

Export to calendar


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.