The course is run online via the Zoom video conferencing system. You need to register and login to see the forum, the Zoom links, and the lecture materials. All news are communicated via the forum.
Office hours helping with the installation of the Coq proof assistant are on April 12 and 13, at 11.15 am. Please make sure you have the Coq proof assistant working before the first lecture, wich is on April 14 at 12.15 pm.
The course is an introduction to basic logic principles, computational type theory, and interactive theorem proving with the proof assistant Coq. At Saarland University we are 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.
Computational 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. Computational type theory is designed such that the correctness of definitions and proofs can be checked automatically.
Coq is an implementation of a computational type theory with expressive inductive types and an impredicative universe of propositions. 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 computational 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 Natural Deduction (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
Lectures take place via Zoom as follows:
- Wednesdays, 12:15 - 13:45
- Fridays, 14:15 - 15:45
The first lecture is on Wednesday, April 14th.
Every student is expected to have a working Coq environment before the first lecture. Assistance for the installation will be provided in the first office hours.
Tutorials
There are weekly tutorials. The tutorials are on Thursdays with the first tutorial on April 22nd. According to their preferences, students are distributed over the following slots:
- Thursdays, 08:30 - 10:00
- Thursdays, 10:15 - 11:45
- Thursdays, 12:15 - 13:45
In the tutorials, you can
- discuss sample solutions to assignments with your tutor and your fellow students, and
- get hints and suggestions concerning the lecture.
Tests
Tests allow you to practice your skills in an exam-like situation.
- Tests will be offered on Tuesdays at 16:00.
- Tests are written and closed-book, and examine the contents of the current assignment sheet.
- Tests should take 15 minutes. Under the current circumstances, you have time to submit each finished test until 00:00.
- To prepare for the tests, you should work through the assignments, and use the office hours and the forum to discuss anything that is unclear to you.
Tests are 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.
Office Hours
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, or
- ask advanced questions about the contents of the lecture.
Office hours will take place on Mondays and Tuesdays at 11:15 (see timetable).
Forum
We offer a forum for the course.
All official announcements concerning the course will be made through the forum exclusively. Therefore we require all students attending the course to subscribe to the forum and read the relevant sections regularly.