Contents of the course
1. Foundations of interactive theorem proving
. The Coq System
. Curry-Howard Correspondance:
. Propositional Logic
. Arithmetic
. Polymorphism
2. Foundations of automatic theorem proving
. Sequent calculus
. Hebrand’s theorem
. The resolution method
The web page of the course is here.
Teaching personnel
- Colin Riba, lecturer, ENS Lyon
- Simon Castellan