Abstract
Coq is a formal proof management system. It consists of a formal language for writing mathematical definitions, algorithms, and theorems, together with an environment for interactive development of formal proofs. This tutorial will focus on introductory topics: proofs of propositional and first order statements; writing functional algorithms as recursive functions and their expected properties as theorems; and proving the said theorems by induction. After a brief introduction a and few exercices that I will run interactively, you will take over and, with my help, are expected to solve the rest of the exercices. Pre-requisites are minimal: basic notions of logic and functional programming. Please have the latest Coq version installed on your laptop, together with the GUI of your choice. Installation instructions are available here.
Short bio
Vlad Rusu is a researcher at Inria Lille, France. Before that, he obtained his PhD at the University of Nantes and spent 18 months as a postdoc at SRI International, Palo Alto, California. His main research interest concerns formal methods and their application to the analysis and verification of safety-critical systems. In the last few years he has been working on extending the class of functions and proofs that can be accepted by the Coq proof assistant and on using Coq for proving the correctness of system-level code.
