INF551 – Computational logic: from Artificial intelligence to Zero bugs

Course

  1. Functional programming
  2. Natural deduction
  3. Pure λ-calculus
  4. Simply typed λ-calculus
  5. Agda
  6. 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.

  1. Typing a simple programming language
  2. Satisfiability of boolean formulas
  3. The λ-calculus
  4. Implementing a propositional prover
  5. Propositional logic in Agda
  6. Inductive types (over two sessions)
  7. Sorting (over two sessions)

References

OCaml

Agda

Other