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

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.

- Exercises on basic logical proofs (the solution to these exercises is given on the Coq'Art site).
- 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.)
- Programming language semantics (this file also contains the full solution and exercises can be made by redoing some of the proofs.)
- 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.

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

Last modified: Fri May 30 09:07:42 CEST 2008