Introductory course on Coq/Gallina

abstract

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

Programming

Describing simple functional programs in the gallina language

• slides
• examples (sorting, computing integers)
• exercises, solutions

Logic and specification

• slides
• examples
• exercises, solutions

Proving properties of programs

• slides
• examples: proofs by reflection, proofs of sorting algorithms
• exercises, solutions, solution to the convolute exercise, solution to the question on irrational square roots

Advanced data-types

• slides
• examples programming with dependent types
• exercises, solutions