After successful completion of the course, students are able to understand and use the Coq proof assistant; in particular to formalize propositional logic, quantifiers inductive types and inductive predicates
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching.
To follow the lessons students need: - a computer - a microphone and headphones (mandatory) - headphones to avoid audio feedback/larsen effect - camera is a plus - but we will certainly not use it much to save bandwith - the Discord app: discordapp.com - free of charge, allows screen sharing - works in a navigator (tested on Chrome) - standalone apps for linux, windows & ios - need to register a (free) account on discordapp.com - the account of the teacher is: Dominique Larchey-Wendling#0283- For lab. sessions, the students need to install Coq and CoqIDE on their own computer - no need to get the latest version (v8.11) - anything above Coq 8.8 (3 years old) will work - the Coq main site: coq.inria.fr - for Linux, try in that order: 1/ install coq & coqide available for your distribution 2/ https://github.com/coq/coq/wiki/Installation-of-Coq-on-Linux 3/ or install it through opam 2 (for experts) - installing Coq for Windows or Mac users: - there are packages in here - https://github.com/coq/coq/releases/tag/V8.11.0
The course will be held blocked May-June
Ects Breakdown 8.0 h attendance of lecture (4 days x 2h) 8.0 h self study at home (4 x 2h) 8.0 h attendance to lab sessions (4 days x 2h) 8.0 h homework (4 x 2h)32.0 h project preparation 1.0 h project presentation 9.0 h preparation for oral exam 1.0 h oral exam-----------------------------------------------75.0 h = 3 Ects
To be decided
Recommended reads: - (short): https://coq.inria.fr/a-short-introduction-to-coq - (less short): the first 20 pages of C. Paulin's introduction course https://www.lri.fr/~paulin/LASER/course-notes.pdf - (reference): The Coq'Art book, https://www.labri.fr/perso/casteran/CoqArt - their are many Coq courses available online - (see eg.) https://github.com/coq/coq/wiki/CoqInTheClassroom - we will roughtly follow the course of P. Casteran: - slides and lab sessions - https://www.labri.fr/perso/casteran/FM/Logique