From Monday December 4 to Friday December 8, 2017, Yves Bertot, Cyril Cohen, Laurence Rideau, Enrico Tassi and Laurent Thery will be teaching a course entitled
“ADVANCED SOFTWARE VERIFICATION AND COMPUTER PROOF”
in Sophia Antipolis.
This course introduces advanced formalization techniques for the Coq proof assistant. In particular students will learn the SSReflect proof language and the Mathematical Components library. Such piece of technology is at the base of large formalizations like the Four Color Thereom or the Odd Order Theorem, and encompasses a proof language designed to write concise and robust proof scripts (called SSReflect) and a huge, modular, library of Coq theories (the Mathematical Components library).
Objective: At the end of the week, we expect that students will know how to write algorithms and proofs on top of the Mathematical Components library and the SSReflect proof language, taking advantage of the large corpus of already formalized algorithms and mathematical results.
Prerequisites: students are expected to have (basic) experience with Coq. No previous knowledge of SSReflect or the Mathematical Components library is expected.
Lessons: the course is organized in the following 8 sessions, each divided into 1h lesson and 1:30 practical exercises.
4/12/2017 – 14:00-17:00 – Enrico Tassi: Intro: SSReflect and the MathComp library
5/12/2017 – 9:00-12:00 – Enrico Tassi: Basic data types
5/12/2017 – 14:00-17:00 – Yves Bertot: Finite types and big operators
6/12/2017 – 9:00-12:00 – Laurent Thery: Arithmetics
6/12/2017 – 14:00-17:00 – Cyril Cohen: The algebra library
7/12/2017 – 9:00-12:00 – Laurence Rideau: Polynomials
7/12/2017 – 14:00-17:00 – Cyril Cohen: Matrix library
8/12/2017 – 9:00-12:00 – Exam, aka long exercise
Courses will take place from Monday 14:00 to Friday 12:00 (the other days of the week 9:00 to 12:00 and 14:00 to 17:00) and will alternate lectures with hands-on exercises for all students. The course is in English and will be located at Inria Sophia Antipolis, in room Coriolis (Galois building), this is very close to the entrance office of the Inria research center (Global coordinates: 43.61472,7.06771).
If you are a doctoral student in computer science or mathematics, not already specializing in computer-based proofs, you will be able to validate credits for this course, as long as you show up to most of the sessions during the week.
Setup: we expect anybody attending to come with a laptop computer equipped with a web browser recent enough to run the test page. Alternatively one can have Coq 8.7 and SSR/MC 1.6 installed, either from pre-compiled versions (as provided by Debian or other Linux distributions) or as re-compiled from the sources: Coq and SSR/MC.
Registration: If you wish to attend, it is preferable that you send a mail to Enrico Tassi and Nathalie Bellesso (all mail addresses are email@example.com ), so that we can plan the size of the required room and we can warn you about changes in the organization. In this application mail, please indicate if you wish some help for accommodation.