COURSE 2018-2019
From Monday November 26 to Thursday November 29, 2018, Yves Bertot, Cyril Cohen, Laurence Rideau, Enrico Tassi and Laurent Thery will be teaching a course entitled
“SOFTWARE VERIFICATION AND COMPUTER PROOF”
in Sophia Antipolis.
This course introduces 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: No previous knowledge Coq, 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.
26/11/2018 – 9:00-12:00 – Functions and computations (slides, exercises , solutions)
26/11/2018 – 14:00-17:00 – First steps in formal proofs (slides, exercises, solutions)
27/11/2018 – 9:00-12:00 – A few more steps in formal proofs (slides, exercises, solutions)
27/11/2018 – 14:00-17:00 – Type theory (slides, exercises, solutions)
28/11/2018 – 9:00-12:00 – Boolean reflection (slides, exercises, solutions)
28/11/2018 – 14:00-17:00 – Real proofs, finally! (slides, exercises, solutions)
29/11/2018 – 9:00-12:00 –Generic theories (slides, exercises, solutions)
29/11/2018 – 14:00-17:00 – Subtypes (slides, exercises, solutions)
Courses will take place from Monday 9:00 to Thursday 17:00 (each day from 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 Kahn 1, this is very close to the entrance office of the Inria research center (Global coordinates: 43.61547,7.06818).
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.8 and SSR/MC 1.7 installed: 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. The school is free of charge.
