News and Events: Upcoming Events

Please note that this newsitem has been archived, and may contain outdated information or links.

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

Speaker: Daniil Frumin (ILLC)
Title: Introduction to Coq proof assistant
Date: Friday 24 April 2015
Time: 18:00-19:00
Location: ILLC Seminar Room (F1.15), Science Park 107, Amsterdam
Target audience: MSc Logic and PhD students

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

Please note that this newsitem has been archived, and may contain outdated information or links.