# INF551 – Computational logic: from Artificial intelligence to Zero bugs

Computational logic has been used in a wide range of application in computer science, ranging from the deductive approach to Artificial Intelligence advocated by AI’s founder John McCarthy, to proving the absence of bugs in large industrial software such as the 14th metro line in Paris, or checking difficult theorems the as the one of Feit-Thompson in the classification of finite simple groups.

The goal of this course is to explain how logic can be used in order for modeling problems of computational or mathematical nature, and how computers can be used to achieve this. In particular, we will present proof assistants, which allow to formalize human reasoning by interactively constructing proofs, and explain their use to certify the absence of bugs in programs.

This is based on the so-called Curry-Howard correspondence: a program is the same as a proof (or, more precisely, a typed functional program corresponds to a derivation of its type). We will gradually introduce the required notions:

- propositional logic and the constructive variants,
- functional programming, formalized by lambda-calculus,
- typing systems and the Curry-Howard correspondence.

Then in order to reach realistic applications, we will present the proof assistant Agda and dependent logic which underlies it. Time permitting, we will also present various important related notions and techniques such as set theory or homotopy type theory.

This course is also about logic in practice: all the TDs will be on computer, using OCaml and then Agda.

Pre-requisites: some basic knowledge of logic, the INF412 course being perfect for this, otherwise reading some introductory book on logic over the summer is recommended (see the references below).

## Course notes

The course notes are available here.

You can order a printed copy on Amazon (bibtex).

## Slides

Here are the slides for the course:

- Functional programming
- Natural deduction
- Pure λ-calculus
- Simply typed λ-calculus
- Agda
- First-order logic
- Dependent types
- Homotopy types

## TD

Before beginning with the first TD, you are advised to read getting started with OCaml if you are not so familiar with this language.

- Typing a simple programming language
- Satisfiability of boolean formulas
- The λ-calculus
- Implementing a propositional prover
- Propositional logic in Agda
- Inductive types (over two sessions)
- Sorting (over two sessions)
- Typing a simple programming language (again)

## References

Apart from the course notes, good references on the subject include:

- Girard:
*Proofs and Types* - Girard:
*The Blind Spot*/*Le Point Aveugle* - Leroy:
*Programmer = démontrer ? La correspondance de Curry-Howard aujourd’hui* - Pierce: Types and Programming Languages
- Selinger:
*Lecture notes on the lambda calculus* - Sørensen and Urzyczyn:
*Lectures on the Curry-Howard isomorphism* *Homotopy Type Theory: Univalent Foundations of Mathematics*aka*The HoTT book**Software foundations*

## Planning

The course takes places on Friday afternoon, in the Turing building. Here is the provisional planning:

Date | From | To | Where |
---|---|---|---|

24/09/2021 | 14:00 | 16:00 | Salle Nicolaas Govert de Bruijn |

24/09/2021 | 16:15 | 18:15 | Salle Rosalind Franklin |

01/10/2021 | 14:00 | 16:00 | Salle Nicolaas Govert de Bruijn |

01/10/2021 | 16:15 | 18:15 | Salle Rosalind Franklin |

08/10/2021 | 14:00 | 16:00 | Salle Nicolaas Govert de Bruijn |

08/10/2021 | 16:15 | 18:15 | Salle Rosalind Franklin |

15/10/2021 | 14:00 | 16:00 | Salle Nicolaas Govert de Bruijn |

15/10/2021 | 16:15 | 18:15 | Salle Rosalind Franklin |

22/10/2021 | 14:00 | 16:00 | Salle Nicolaas Govert de Bruijn |

22/10/2021 | 16:15 | 18:15 | Salle Rosalind Franklin |

05/11/2021 | 14:00 | 16:00 | Salle Nicolaas Govert de Bruijn |

05/11/2021 | 16:15 | 18:15 | Salle Rosalind Franklin |

12/11/2021 | 14:00 | 16:00 | Salle Nicolaas Govert de Bruijn |

12/11/2021 | 16:15 | 18:15 | Salle Rosalind Franklin |

19/11/2021 | 14:00 | 16:00 | Salle Nicolaas Govert de Bruijn |

19/11/2021 | 16:15 | 18:15 | Salle Rosalind Franklin |

26/11/2021 | 14:00 | 16:00 | Salle Nicolaas Govert de Bruijn |

26/11/2021 | 16:15 | 18:15 | Salle Rosalind Franklin |

## Links

### General

- the DIX Slack workspace:
ask any question on the
`#inf551`

channel

### OCaml

- OCaml
- OCaml’s documentation
- OCaml’s standard library
- Real World OCaml: a book about OCaml from the beginning

### Agda

- Agda
- Agda’s documentation
- Agdapad: an online emacs emulation for Agda

### Editors

### Other proof assistants

### Additional resources

### Where to find internships

Research labs:

- CEA LIST (in particular Frama-C)
- Data61: Trustworthy Systems
- IRIF: Preuves et programmes
- Inria: Gallinette
- Inria: Marelle and πr²
- Inria: Toccata
- LRI: VALS
- ProofInUse
- SRI

Companies:

Topics:

- compilers: CompCert, DeepSpec, Verified Software Toolchain, CompCert TSO

Other resources:

### Where to find master 2 courses

If you liked this course I would strongly recommend that you follow the MPRI next year. In particular, the following courses are about closely related topics:

- 2.1:
*Linear logic and logical paradigms of computation* - 2.2:
*Models of programming languages: domains, categories, games* - 2.4:
*Functional programming and type systems* - 2.5.1:
*Automated deduction* - 2.6:
*Abstract interpretation: application to verification and static analysis* - 2.7.1:
*Foundations of proof systems* - 2.7.2:
*Proof assistants*

(this is especially true for 2.4, 2.7.1 and 2.7.2).

Other interesting and related masters abroad include:

- the MSc in Mathematics and Foundations of Computer Science in Oxford
- the MPhil in Advanced Computer Science in Cambridge
- the MSc in Compute Science in Carnegie Mellon University