# 192.098 Introduction to the Coq proof assistant This course is in all assigned curricula part of the STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_20",{id:"j_id_20",showEffect:"fade",hideEffect:"fade",target:"isAllSteop"});});This course is in at least 1 assigned curriculum part of the STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_22",{id:"j_id_22",showEffect:"fade",hideEffect:"fade",target:"isAnySteop"});});

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

## 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
- 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

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

## Course registration

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

## Literature

No lecture notes are available.

## Previous knowledge

- (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

English