The course is an introduction to basic logic principles, computational type theory, and interactive theorem proving (using the Coq proof assistant). At Saarland University, we are teaching this course since 2010. We expect students taking the course to be familiar with the basic ideas of mathematical reasoning and functional programming. The curriculum of of our Bachelor's Programs is such that talented students may take the course in their second semester.
Computational type theory provides a framework and a programming language for developing mathematical and computational theories. Theories consist of definitions and theorems stating logical consequences of the definitions. Theorems come with proofs ensuring the correctness of their statements. Computational type theory is designed such that the correctness of definitions and proofs can be checked automatically.
The Coq proof assistant we are using in this course is an implementation of a computational type theory with expressive inductive types providing for intuitionistic and classical reasoning. Coq is designed as an interactive system assisting the user in developing theories. The most interesting part of the interaction is the construction of proofs. In the course we use Coq from day one. Coq is a mature system originating in the 1980's. In recent years Coq has become a popular tool for research and education in formal theory development and program verification.
Coq is the applied side of the course. On the theoretical side we explore the basic principles of computational type theory, which are essential for programming languages, proof systems, and the foundation of mathematics.
Textbook
The course will follow the MPCTT textbook.
Proof Assistant
We will use the Coq proof assistant throughout the course. Every student is expected to have Coq installed. Directions for installation are at the Coq site. Beginners are encouraged to use one of the binary installers (MacOs, Windows, Linux) and the accompanying CoqIDE. Help with the installation will be given in the office hours of the first week.
Lectures
Also see the timetable for an overview of lectures, tutorials and office hours.
Lectures are on Wednesday (12.15 - 13.45) and on Friday (14.15 - 15.45) during the lecture period (April 11 - July 22). The first lecture is on April 13. Lectures will take place in HS 002 in Building E1 3 and will be streamed through Zoom. Recordings of the lectures will be provided.
Tutorials
There are weekly tutorials where you discuss the exercise assignment with the tutor and fellow students. The tutorials are on Tuesdays at 10.15 - 11.45 and 14.15 - 15.45, with the first tutorial on April 26. You will be able to indicate your preferences during registration. The tutors are Benjamin Peters and Marc Hermes. The tutorials take place in Room SR 015 in Building E1 3. At the moment, we do not plan to offer a hybrid or an online tutorial.
Office Hours
The office hours are walk-in and are the place where you can discuss all aspects of the course with the tutors. You may ask for help with particular topics you find difficult to understand. All questions concerning the course and the proof assistant are welcome. The office hours are on Mondays (15.01 - 16.00) and Thursdays (10.01 - 11.00). The Monday slot is replaced by an office hour Tuesdays 15.01 - 16.00 for the first two weeks. Starting with the second week, the office hours are in Room 525 in Building E1 3 and on request also via Zoom.
During the first week (April 11 - 15), the office hours are via Zoom only and concentrate on first steps with the proof assistant Coq. You can find the Zoom room here.
Assignments
There will be weekly exercise assignments that help you understand the material and prepare you for the exam. You are supposed to work on the problems on the assignments using the lecture notes. You may discuss the problems with fellow students and the tutors. In the end, you should be able to solve all problems on the assignments on your own. The weekly assignments will be posted on Friday, with the first assignment in the second week.
Tests
Starting with the third week, we will write weekly tests on Wednesday at the beginning of the lecture (12.15) in the lecture hall. A test lasts 15 minutes and consists of one sheet you fill in by handwriting. A test checks your understanding of the material of the assignment from the previous Friday. With each test you can earn 15 points. You need 33% of the points of the test to be admitted to the exam. The graded tests will be returned in the tutorials.
Exam
There will be an oral exam after the lecture period determining your grade. Each participant will be assigned a 30 minutes slot on either August 31 or September 1st.
Registration
To take the course, you need to register with the CMS (see menu at the top). Registration is open April 4.-20. To get credit for the course, you will have to register with the LSF of the university for the exam.
Forum
There is a forum for the course (see menu at the top). To see the forum you need to register with the CMS. All announcements concerning the course will be made in the forum. The forum serves as a discussion board for all questions concerning the course.