The course is an introduction to basic logic principles, constructive type theory, and interactive theorem proving with the proof assistant Coq. At Saarland University we teach the course in this format since 2010. Students are expected to be familiar with mathematical definitions and proofs and to know some functional programming. The curriculum of the Bachelor's Program of Saarland University is such that talented students can take the course in their second semester.
Constructive type theory provides a programming language for developing mathematical and computational theories. Theories consist of definitions and theorems, where theorems state logical consequences of the definitions. Every theorem comes with a proof justifying it. If the proof of a theorem is correct, the theorem is correct. Constructive type theory is designed such that the correctness of definitions and proofs can be checked automatically.
Coq is an implementation of a constructive type theory known as the calculus of inductive definitions. Coq is designed as an interactive system that assists the user in developing theories. The most interesting part of the interaction is the construction of proofs. The idea is that the user points the direction while Coq takes care of the details of the proof. In the course we use Coq from day one.
Coq is a mature system whose development started in the 1980's. In recent years Coq has become a popular tool for research and education in formal theory development and program verification. Landmarks are a proof of the four color theorem, a proof of the Feit-Thompson theorem, and the verification of a compiler for the programming language C (COMPCERT).
Coq is the applied side of this course. On the theoretical side we explore the basic principles of constructive type theory, which are essential for programming languages, logical languages, proof systems, and the foundation of mathematics.
An important part of the course is the theory of classical and intuitionistic propositional logic. We study various proof systems (Hilbert, ND, tableaux), decidability of proof systems, and the semantic analysis of proof systems based on models. The study of propositional logic is carried out in Coq and serves as a case study of a substantial formal theory development.
Lectures are on Tuesdays and Thursdays, 12:15 - 13:45, in Building E1 3, lecture hall HS002. The first class is on Tuesday, April 19. There will be no class on Thursday, May 5, and Thursday, May 26, since these are official holidays.
There will be weekly tutorials. The tutorials will be on Wednesdays with the first tutorial on Wednesday, April 27. There will be two tutorials:
- Tutorial 1: Wednesday, 10:15 - 12:00, U.36, E2 5.
- Tutorial 2: Wednesday, 12:15 - 14:00, U12, E1 1.
In the tutorials, you can
- test your knowledge in an exam-like situation (tests, see below),
- discuss the sample solutions to the assigments with your tutor and your fellow students, and
- get hints and suggestions concerning the lecture.
A tutorial usually takes about 90 minutes.