2010, August 20-27, Tsinghua University, Beijing
Contact: coqschool@formes.asia
I repeat: contact address is coqschool@formes.asia
This summer school shall be the second summer school of this kind to be held in China. It will take place at the School of Software of Tsinghua University. The objective is to teach students the principles and practice of programming with the proof assistant Coq, like last year, and to provide them with a solid background on its foundations, i.e. higher-order logic, induction and type theory.
Coq is a free, open source software developed at INRIA, Université Paris-Diderot, Université Paris-Sud, CNRS, CNAM and École Polytechnique in France.
The Coq system provides a functional programming language and a reasoning framework based on higher order logic to perform proofs of programs. The expressive power of the language is such that advanced notions of mathematics (such as the graph theory in the four color theorem) or programs of high complexity (such as a compiler for a significant kernel of the C Programming language) can be described formally. In this school, we address the basic programming techniques and approaches to prove properties of the programs. The covered notions involve structural recursive programming, list and integer handling, proof by induction, definition of data-types, pattern matching constructs and case-based reasoning, and inductive properties.
We plan to accept at most 55 students, from China and the other Asian-Pacific countries. Courses will be delivered in English. Students are expected to be fresh master students or more, in Computer Science, Software Engineering or Mathematics. No prior knowledge of type theory is required, but a good programming experience is expected.
Students are encouraged to read the Coq tutorial and make the very first easy exercices. Course notes will be distributed at each course.
Classes will be given in parallel to smaller groups of at most 15 students who will work during the class on a PC made available by Tsinghua University.
Resources about Coq can be downloaded from here.
Materials given last year can be found on the 1st Asian-Pacific Coq Summer School.
Registration
The registration process is now closed.
Registration fees for Tsinghua Master, Ph.D. students or Postdoc amounts to 150 RMB, 300 RMB for students from other universities, and 600 RMB for non-students. Registration fees shall be paid in cash upon arrival.
As part of the material, a name tag will be given at the registration desk. Name tags will be mandatory for accessing the classrooms.
Registration fees include the Chinese version of the CoqArt book by Yves Bertot and Pierre Castéran, lunches, breaks, a social event on the free afternoon and the subsequent conference dinner.
For mainland Chinese students housing is provided on demand in Tsinghua's student appartments for free.
Registration fees shall be paid in cash upon arrival.
Acceptation
All notifications have now been sent. The list of participants is available here
Lecturers
Lecturers are Coq experts who have participated to the development of Coq itself or to developments using Coq, and have experience in teaching Coq programming to students. Most lecturers will teach both courses and classes.
| Lecturer | Institution |
|---|---|
| Yves Bertot | Research Director, INRIA & MSR-INRIA Joint Center |
| Pierre Castéran | Professor, University of Bordeaux I |
| Frédéric Blanqui | Researcher, INRIA & Tsinghua University |
| Jean-Pierre Jouannaud | Research Director, INRIA & Tsinghua University |
| Jean-Jacques Lévy | Research Director, INRIA & MSR-INRIA Joint Center |
| Jean-François Monin | Professor, University of Grenoble I, CNRS & Tsinghua University |
| Sandrine Blazy | Professor, University of Rennes I |
| Instructor | Institution |
|---|---|
| Jian-Qi Li | Post-Doc, Tsinghua University |
| Huiying Luo | Ph.D. student, Tsinghua University |
| Sidi Ould-Biha | Post-Doc, INRIA & Tsinghua University |
| Xiaomu Shi | Ph.D. student, Université de Grenoble I |
| Qian Wang | Ph.D. student, Tsinghua University |
| Lianyi Zhang | Ph.D. student, Tsinghua University |
Program
Mornings are dedicated to lectures: one lecture on foundations and one lecture on Coq. Afternoons are dedicated to exercises on Coq.
- Friday 20 August:
- 09:00: Lecture 1: introduction to first-order logic, Jean-Pierre Jouannaud
- 10:30: Lecture 2: introduction to Coq, Yves Bertot
- 14:00: Exercises on Coq
- Saturday 21 August:
- 09:00: Lecture 3: induction on natural numbers, Jean-Francois Monin
- 10:30: Lecture 4: programming on natural numbers and lists in Coq, Pierre Castéran
- 14:00: Exercises on Coq
- Sunday 22 August:
- 09:00: Lecture 5: structural induction, Jean-Francois Monin
- 10:30: Lecture 6: propositional logic in Coq, Pierre Castéran
- 14:00: Exercises on Coq
- Monday 23 August:
- 09:00: Lecture 7: introduction to untyped lambda-calculus, Jean-Jacques Lévy
- 10:30: Lecture 8: first-order logic and equality in Coq, Yves Bertot
- 14:00: Visit of the Summer Palace
- 19:00: Diner in a restaurant
- Tuesday 24 August:
- 09:00: Lecture 9: confluence and standardization of the untyped lambda-calculus, Jean-Jacques Lévy
- 10:30: Lecture 10: proving the correctness of programs in Coq, Yves Bertot
- 14:00: Exercises on Coq
- Wednesday 25 August:
- 09:00: Lecture 11: introduction to the simply-typed lambda-calculus, Frédéric Blanqui
- 10:30: Lecture 12: inductive types in Coq, Pierre Castéran
- 14:00: Exercises on Coq
- Thursday 26 August:
- 09:00: Lecture 13: termination of the simply-typed lambda-calculus, Frédéric Blanqui
- 10:30: Lecture 14: inductive predicates in Coq, Pierre Castéran
- 14:00: Exercises on Coq
- Friday 27 August:
- 09:00: Lecture 15: Curry-Howard correspondence, Jean-Pierre Jouannaud
- 10:30: Lecture 16: introduction to dependent types in Coq, Yves Bertot
- 14:00: Lecture 17: presentation of Compcert, a Coq-certified C compiler, Sandrine Blazy
