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.


Here are some of the slides

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.


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

From left to right: Zhu JianZhong, Wang Xiuqun, Liu Liu, Wang Rui, Zhou Min, Yves Bertot, Benjamin Werner, Zhang Lianyi, Zhang Hehua, Wan Hai (not in this picture, but in the others, Li Jian-Qi).

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