Coq course at Tsinghua University, Beijing

Have a look at the poster of the course.

During the week from April 7 to April 11, Benjamin Werner and Yves Bertot gave a course on Coq at Tsinghua University in Beijing. This page gathers most of the material we used for this course.

There were 5 morning sessions, in the form of lectures with computer support (slideshows) and 4 afternoon sessions in the form of practice sessions. For the practice sessions we expected each student to work with Coq on their own computer. All computers had a laptop using CoqIde. My exercises could all be run on CoqV8.1pl2. Apparently, no student had to suffer from a difference in Coq version.

Lectures

Here are some of the slides

• First lecture (3 hours): Introduction to dependent types and their use in proofs
• Third lecture (3 hours): Using inductively defined predicates. This lecture also contained a demonstration about the benefits of using inductive predicates and their induction principles to conduct proofs about sorting algorithms.
• Fifth lecture (1 to 2 hours): Formalizing non-structural induction and well-founded induction. For this course, there is a little example developed in Coq about using the Function command to encode the merge function and proving that this preserves sorting.
• Sixth lecture (1 hour): automatic proof tactics. This lecture also uses a small example file.

Practice sessions

1. Exercises on basic logical proofs (the solution to these exercises is given on the Coq'Art site).
2. Proving a program correct: sorting (this file contains the full solution, to make it into a exercise file, all proofs should be removed, by removing the text between "Proof." and the corresponding "Qed." keywords.)
3. Programming language semantics (this file also contains the full solution and exercises can be made by redoing some of the proofs.)
4. simple mathematical proofs. We asked the students to write a program that computes the sum of the n first integers and to prove that this sum satisfies the well-known mathematical formula. Then we asked the students to define the function that computes the binomial coefficients (also known as the number of combinations of p elements taken among n) and to prove the well-known formula with respect to factorials. The file provided here does not give the solution to the first problem, but a solution to a similar problem (the sum of the n first squares) and the solution to the second problem.

Pictures

This course was an occasion to meet great people. We have a few photographs in a zip archive, with a few group pictures: