Introductory course on Coq/Gallina


Coq is a system to write programs and verify that they work as expected.

It is based on the calculus of inductive constructions, a variant of Type Theory. It makes it possible to describe programs in three steps:

  1. write how the program operates
  2. write what the program is supposed to do as a logical statement between inputs and outputs
  3. write a proof showing that the program really does what is specified

There are several proof systems that make it possible to perform these three steps. What distinguishes Coq is a particular effort to support large scale efforts. Coq can produce software that is used in real life.

This page collects the material for an introductory course on Coq consisting of approximately 3 hours, plus material for exercises and experiments.

A longer tutorial is available in Coq in a hurry


Describing simple functional programs in the gallina language

Logic and specification

Proving properties of programs

Advanced data-types