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.

Proofgeneral problems on Debian/Ubuntu

Unfortunately, it seems that the proof general installed through the system package manager (of certain Ubuntu and Debian releases) is often problematic. I have made a minimal init.el, which is essentially from the proof general website, that configures your emacs appropriately. It configures emacs to use the melpa package repository instead of the system repository. You still need to start your emacs and install the proof general. See the proof general website website for more details

mkdir ProofPrograms
cd ProofPrograms
git clone https://bitbucket.org/piyush-kurur/ppt  # Clone this repository


mkdir -p ~/.emacs.d  # Create the emacs.d directory if it does not exists.
cp init.el ~/.emacs.d/ # This will overwrite your emacs config file if there is one

# Start emacs and install the packages using
#
# M-x package-refresh-contents RET
# M-x package-install RET proof-general RET

Note M-x means type Alt-x followed by the command given above (you can use tab to complete the command form a prefix).