COURSE 2017-2018
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
Tactics, notations, principles of Small Scale Reflection and the Mathematical Components library (lesson, exercise session, exercise template, exercise solution, cheat sheet)
-
5/12/2017 – 9:00-12:00 – Enrico Tassi: Basic data types
Basic data types like natural numbers and lists and their associated library (lesson, exercise session, exercise template, solution)
-
5/12/2017 – 14:00-17:00 – Yves Bertot: Finite types and big operators
Handling notions of finiteness and finitely iterated operations (lesson, exercise session, exercise template, exercise solution)
-
6/12/2017 – 9:00-12:00 – Laurent Thery: Arithmetics
Order, division, primality (lesson, exercise session)
-
6/12/2017 – 14:00-17:00 – Cyril Cohen: The algebra library
Interfaces and instances of the algebra library; notations and theorems about rings (lesson, exercise session, exercise template)
-
7/12/2017 – 9:00-12:00 – Laurence Rideau: Polynomials
Polynomials: data structure, algorithms and proofs (lesson, exercise session, exercise template)
-
7/12/2017 – 14:00-17:00 – Cyril Cohen: Matrix library
Matrices and related algorithms (lesson, lesson sources, exercise session, exercise template)
-
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 firstname.name@inria.fr ), 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.
