Core Course, 9 credit points
Prof. Gert Smolka,
Dr. Chad E Brown
Department of Computer Science,
Saarland University
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 Mondays and Wednesdays, 12.15–13.45, in Building E2 2 (Günter Hotz Hörsaal). See also the timetable page. The first class is on Wednesday, April 17. There will be no class on Wednesday, May 1, and Monday, May 20, since these are official holidays.