Clone wiki

ppt / Home

Programs, Proofs and Types: Course wiki

In this course, we study how to write certified programs, i.e. programs together with proofs that they indeed satisfies the requirements of the programs. The proofs are formal, in the sense that their correctness checked by the computer itself. The course uses the proof assistant Coq for this course.

A quick description of Coq and similar systems.

The underlying theory of proof assistants like Coq is a theory of depenent types. One can see such systems as a (functional) programming language with very advanced type. The specifications that the program has to satisfy can be expressed as types in the programming language and proving that a program satisfies a specifications is to write a program of the appropriate type. Thus writing proofs are closely related to programming. Due to the close connections to functional programming, these systems allow ``extracting'' programs which can then be compiled and run.

While our main motivation in this course is the write programs that are formally proved to be correct, systems like coq can be used to formalise and prove mathematical theorems as well.

Getting started.

You need to have a working environment suitable for using Coq. I would recommend installing one of the standard GNU/Linux distributions. Coq comes pre-packaged in most of them. Here are some instructions for getting coq up and running on Debian/Ubuntu

$ sudo apt-get install coq          # Install coq
$ sudo apt-get install emacs        # If you do not have it already
$ sudo apt-get install proofgeneral # The proof general mode for emacs

Coq comes with an IDE. While it is okey for basic interaction, any nontrivial development will require you to use an editor with good support for coq. Emacs has very good support for coq via the proof general mode. This is what I recommend for day to day use.

Note: If you have managed to get other editors, vim for example, to work well with coq please include the details here in the wiki.