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 have been teaching 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 constructions. 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 formalize ND proof systems in Coq and show that classical ND reduces to intuitionistic ND. Using a DNF-based solver and a tableau system, we show that provability in the classical ND system is interreducible with boolean unsatisfiability.
Lectures are on Wednesdays, 16:00-17:30, and Thursdays, 12:15 - 13:45, in Building E1 3, lecture hall HS 002. The first lecture is on Wednesday, April 10. There will be no class on Wednesday, May 1, on Thursday, May 30, and on Thursday, June 20, since these are official holidays. The last class on Thursday, July 18, will be in lecture hall HS 003.
There will be weekly tutorials. The tutorials will be on Tuesdays with the first tutorial on April 16. The students will be distributed according to their preferences on two slots out of the following three options:
- Tuesdays, 8:30 - 10:00, Building E1 3, SR 014
- Tuesdays, 12:15 - 13:45, Building E1 3, SR 014
- Tuesdays, 14:15 - 15:45, Building E1 3, SR 014
In the tutorials, you can
- test your knowledge in an exam-like situation (tests, see below),
- discuss the sample solutions to the assignments with your tutor and your fellow students, and
- get hints and suggestions concerning the lecture.
A tutorial usually takes about 90 minutes.
Tests allow you to practise your skills in an exam-like situation.
Tests will be offered at the beginning of each tutorial. They are written and closed-book, and examine the contents of the current assignment sheet. Tests will take 15 minutes. To prepare for the tests, you should work through the assignments, and use the office hours and the discussion board to ask about anything that is unclear to you.
Tests will be graded. In each test you can gather up to 15 points. Missing a test gets you 0 points for that test.
You need to gather a certain minimum of points in the tests to be admitted to the exams. See the exams page for details.
Your test scores can be found on your personal status page.
During the office hours, you can get direct support. You may, for example, want to
- resolve individual problems you might have with the lecture,
- discuss alternative solutions to the assignments,
- ask advanced questions about the contents of the lecture.
Office hours will normally take place on Mondays, 12:15 - 13:45, in Room 528 of Building E1 3. There might be additional office hours which you can find on the Timetable.
We offer a discussion board for the course.
All official announcements concerning the course will be made through the board exclusively. Therefore we require all students attending the course to subscribe to the board and frequently read the relevant sections.