Universiteit van Amsterdam

Events

Institute for Logic, Language and Computation

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.