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
Here are some of the slides
- 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:
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