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

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.