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

## Course

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

Other slides will appear here in due time.

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

## References

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