192.098 Introduction to the Coq proof assistant
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2020S, VU, 2.0h, 3.0EC, to be held in blocked form

Properties

  • Semester hours: 2.0
  • Credits: 3.0
  • Type: VU Lecture and Exercise

Learning outcomes

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

Subject of course

This course gives an introduction to the Coq proof assistant:

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.

4 lecture sessions

  1. Introduction to Coq, Propositional Logic
  2. Quantifiers, equality and all that
  3. Inductive types
  4. Inductive predicates

4 lab sessions

  1. Your first proofs, propositional logic
  2. First Order Logic, Higher Order Logic
  3. Proofs by induction on nat
  4. Proofs by induction on proofs

 

Teaching methods

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

Mode of examination

Immanent

Additional information

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

Lecturers

Institute

Examination modalities

To be decided

Course registration

Begin End Deregistration end
18.03.2020 10:00 04.05.2020 10:00 30.05.2020 10:00

Curricula

Literature

No lecture notes are available.

Previous knowledge

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


Language

English