24 April 2015, Cool Logic, Daniil Frumin (ILLC)

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.

For more information, see http://www.illc.uva.nl/coollogic/ or contact coollogic.uva at gmail.com