1st Asian-Pacific Summer School on Formal Methods

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.

Description

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.

Registration

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.

Acceptation

Notifications have all been sent.

Lecturers

LecturerInstitution
Gilles BartheProfessor, IMDEA Software, Madrid
Yves BertotResearch Director, INRIA Sophia Antipolis, Microsoft Research-INRIA Joint Centre, Orsay
Frédéric BlanquiPh.D., INRIA Rocquencourt, Tsinghua University, Beijing
Pierre CasteranProfessor, Université de Bordeaux I
Guillaume MelquiondResearcher, INRIA Saclay - Île-de-France, LRI, Université Paris-Sud, Orsay
Virgile PrevostoPh.D., CEA-LIST, Saclay
Jean-François MoninResearch Director, CNRS, Tsinghua University, Beijing
Pierre-Yves StrubPh.D., INRIA Rocquencourt & Tsinghua University, Beijing

Instructors

InstructorInstitution
Jian-Qi LiPh.D., Tsinghua University, Beijing
Huiying LuoPh.D. student, Tsinghua University, Beijing
Qian WangPh.D. student, Tsinghua University, Beijing
Lianyi ZhangPh.D. student, Tsinghua University, Beijing

Program

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.

SubjectTeachers
C1-C4BasicsY. Bertot, P. Casteran
C5Dependent typesY. Bertot, P. Casteran
C6Inductive typesY. Bertot
C7Co-Inductive typesP. Casteran
C8-C9SSReflectG. Melquiond
C10-C11WHY toolG. Melquiond, V. Prevosto
C12-C13FRAMA-C toolV. Prevosto
C14Using Coq for smart card applicationsG. Barthe
Classes-F. Blanqui, J-F. Monin, P-Y. Strub, Instructors


Day09:00 - 10:3010:50 - 12:2014:00 - 16:0016:30 - 18:30
Aug 24Course 1BreakCourse 2LunchClass 1BreakClass 2
Aug 25Course 3BreakCourse 4LunchClass 3BreakClass 4
Aug 26Course 5BreakCourse 6LunchClass 5BreakClass 6
Aug 27Course 7BreakClass 7Lunch
Aug 28Course 8BreakCourse 9LunchClass 8BreakClass 9
Aug 29Course 10BreakCourse 11LunchClass 10BreakClass 11
Aug 30Course 12BreakCourse 13LunchClass 12BreakClass 13
Aug 31Course 14BreakClass 14LunchPresentationsBreakPresentations

Presentation of research projects

Aug. 31 afternoon is dedicated to the presentation of Master and Ph.D. projects.

Social Event

A visit of the Summer Palace will take place on Aug. 27, followed by the school diner.

Organisation

WebsitePierre-Yves Strub
SecretaryTang, Lin, CASIA, and Wang, Elizabeth, Tsinghua University
Contactcontact_AT_coqschool-asia.org
pierre-yves_AT_strub.nu

In contact addresses, replace _AT_ by @

School Directors

Ming Gu
Professor, School of Software Director, Tsinghua University, Beijing

Jean-Pierre Jouannaud
Research Director, INRIA Rocquencourt, Formes project Director, Tsinghua University, Beijing



img!tsinghua.png img!inria-msr.png img!inria.png img!anr.png img!nfsc.png img!cnrs.png