Daniil Frumin
(ILLC)
Introduction to Coq proof assistant
April 24th at 18:00, in F1.15 ILLC seminar room
In this talk I will briefly introduce the theory and practice of Coq — a proof assistant based on dependent type theory. A proof assistant is a piece of software that provides you with a semi-interactive environment for constructing and verifying formal proofs. Coq has been used to prove/verify theorems from “pure math” (e.g. odd order theorem), as well as in software verification (verified C compiler).
Feel free to bring your laptops, as the second part of the talk will be a practical hands-on Coq session, during which we will play a bit with Coq, by defining basic datatypes and proving simple properties about them.