August 24-31, Tsinghua University, Beijing
Contact: contact@coqschool-asia.org
I repeat: contact address is contact@coqschool-asia.org
Registrations are now closed. We won't accept any late application.
This summer school shall be the very first summer school of this kind to be held in China, in the Future Internet Technology Research Center (FIT) of Tsinghua University. The objective is to teach students the principles and pratice of programming with the proof assistant Coq, a free, open source software developed at INRIA, Université Paris-Sud and École Polytechnique in France.
We plan to accept at most 60 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 come with their laptop, have the Coq distribution installed before the start of the course, read the tutorial and made 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 their laptop or on a PC made available by Tsinghua University. Chinese students already familiar with Coq will help during the classes.
A few PhD fellowships in France or China will be awarded at the end of the course to students interested in formal methods. Those candidates to a fellowship should come with their credentials: undergraduate grades, 3 letters of recommandation, performance at the national competitions.
Resources about Coq can be downloaded from here.
Registrations are now closed.
Registration fees for Master, Ph.D. or Postdoc students amounts to 100 元, and 500 元 for non-students. Registration fees shall be paid in cash upon arrival.
Registration fees include the chinese version of the CoqArt book by Bertot and Casteran, lunches, breaks, the visit to the Summer Palace on the free afternoon and the subsequent conference dinner.
Housing is provided on demand in Tsinghua’s student appartments for free.
Registration fees shall be paid in cash upon arrival.
Notifications have all been sent.
Lecturer | Institution |
---|---|
Gilles Barthe | Professor, IMDEA Software, Madrid |
Yves Bertot | Research Director, INRIA Sophia Antipolis, Microsoft Research-INRIA Joint Centre, Orsay |
Frédéric Blanqui | Ph.D., INRIA Rocquencourt, Tsinghua University, Beijing |
Pierre Casteran | Professor, Université de Bordeaux I |
Guillaume Melquiond | Researcher, INRIA Saclay - Île-de-France, LRI, Université Paris-Sud, Orsay |
Virgile Prevosto | Ph.D., CEA-LIST, Saclay |
Jean-François Monin | Research Director, CNRS, Tsinghua University, Beijing |
Pierre-Yves Strub | Ph.D., INRIA Rocquencourt & Tsinghua University, Beijing |
Instructor | Institution |
---|---|
Jian-Qi Li | Ph.D., Tsinghua University, Beijing |
Huiying Luo | Ph.D. student, Tsinghua University, Beijing |
Qian Wang | Ph.D. student, Tsinghua University, Beijing |
Lianyi Zhang | Ph.D. student, Tsinghua University, Beijing |
Lecturers are Coq experts who have participated to the Coq project or to Coq developments, and have, for some of them, experience in teaching Coq programming to students. Most lecturers will teach both courses and classes.
Subject | Teachers | |
---|---|---|
C1-C4 | Basics | Y. Bertot, P. Casteran |
C5 | Dependent types | Y. Bertot, P. Casteran |
C6 | Inductive types | Y. Bertot |
C7 | Co-Inductive types | P. Casteran |
C8-C9 | SSReflect | G. Melquiond |
C10-C11 | WHY tool | G. Melquiond, V. Prevosto |
C12-C13 | FRAMA-C tool | V. Prevosto |
C14 | Using Coq for smart card applications | G. Barthe |
Classes | - | F. Blanqui, J-F. Monin, P-Y. Strub, Instructors |
Day | 09:00 - 10:30 | 10:50 - 12:20 | 14:00 - 16:00 | 16:30 - 18:30 | |||
---|---|---|---|---|---|---|---|
Aug 24 | Course 1 | Break | Course 2 | Lunch | Class 1 | Break | Class 2 |
Aug 25 | Course 3 | Break | Course 4 | Lunch | Class 3 | Break | Class 4 |
Aug 26 | Course 5 | Break | Course 6 | Lunch | Class 5 | Break | Class 6 |
Aug 27 | Course 7 | Break | Class 7 | Lunch | |||
Aug 28 | Course 8 | Break | Course 9 | Lunch | Class 8 | Break | Class 9 |
Aug 29 | Course 10 | Break | Course 11 | Lunch | Class 10 | Break | Class 11 |
Aug 30 | Course 12 | Break | Course 13 | Lunch | Class 12 | Break | Class 13 |
Aug 31 | Course 14 | Break | Class 14 | Lunch | Presentations | Break | Presentations |
Aug. 31 afternoon is dedicated to the presentation of Master and Ph.D. projects.
A visit of the Summer Palace will take place on Aug. 27, followed by the school diner.
Website | Pierre-Yves Strub |
---|---|
Secretary | Tang, Lin, CASIA, and Wang, Elizabeth, Tsinghua University |
Contact | contact_AT_coqschool-asia.org |
pierre-yves_AT_strub.nu |
In contact addresses, replace _AT_ by @
Ming Gu
Professor, School of Software Director, Tsinghua University, Beijing
Jean-Pierre Jouannaud
Research Director, INRIA Rocquencourt, Formes project Director, Tsinghua University, Beijing