# 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)

### 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.