‎

1. How to find me and support material
2. On your machine, install
3. Objectives
- 3.1. What do you prefer:
4. An ubiquitous concept coming from computer science: TREES
5. Coq: a proof assistant based on Type Theory

Certified programs and proofs in Coq, OCaml and dependent Type Theory Jean-François Monin, Verimag, Univ Grenoble Alpes jean-francois.monin@univ-grenoble-alpes.fr

Credits. These lectures are mainly based on a course (named LTPF) given in France for about 6 years, and additional material related to my own research. The main part benefited from inputs of the LTPF teaching team. Special thanks to Pierre Corbineau for his contributions.

1 How to find me and support material

search engine -> monin verimag
https://www-verimag.imag.fr/~monin/
   -> Teaching material for students -> ECNU-2024
   https://www-verimag.imag.fr/~monin/Enseignement/ECNU-2024

2 On your machine, install

Coq
OCaml
for editing: coqide or emacs+proof-general

For them opam (pck manager for OCaml) is a good choice.

Possible alternative: vscode.

I use emacs+proof-general (independent from opam).

A basic installation will be enough (otherwise it may take time)

3 Objectives

3.1 What do you prefer:

create an exciting program?
or read/write a boring scientific paper?

3.1.1 If you are in the first category,

Coq is for you.

3.1.2 If you are in the second category,

Coq is for you as well: Supporting paper-and-pencil elliptic "proofs" by a machine-checked formal developement became a standard in prominent conferences such as POPL.

3.1.3 With Coq, doing maths becomes an IA

IA =
Interesting Activity YOU become more intelligent, because you are doomed to UNDERSTAND what you are doing,
- Don't rush on the next exercises. Understand what you are doing, read the feedback of Coq.
- In this course I'll refrain to use dark magics. Everything will be explained in terms of elementary steps that are expected to be easy to follow.
Disclaimer

Using Coq is an addictive game

4 An ubiquitous concept coming from computer science: TREES

data structures e.g. binary trees, lists, Peano natural numbers
AST (Abstract Syntax Trees)
Proofs seen as proof trees
Operational semantics

5 Coq: a proof assistant based on Type Theory

5.1 Proof

It is about mathematical reasoning. Makes sense in (usual) Maths and in Computer Science, which can be seen as a special branch of maths.

We will focus on Computer Science, in particular we will rely on intuitions and knowledge famiiar to programmers: no background on analysis, geometry or even Set Theory is needed. But we expect some familiarity with – data structures, especially recursive data structures such as trees and lists – programming, especially recursive programs (our programs we be called functions) – basic notions on typing, however this topic will be developed a lot.

5.2 Assistant

Coq is a software interactive tool helping the user to develop definitions and theorems in an interactive way. Ideally: clever inputs are entered by the human user, whereas tedious details are machine-checked. In practice: to be discussed; anyway the proof-checking performed in tools like Coq is actually very secure by design. Kernel based.

5.3 Type Theory

An extension of a well-known good practice in programming. The usual tension between benefits and constraints disappears thanks to the power of polymorphism and dependent types. PASCAL ADA.

Table of Contents