The course teaches modelling and proving in computational type theory (a foundational mathematical system) using the interactive theorem prover Coq (a programming system). We explain the design of computational type theory and use it to study computational structures such as natural numbers, lists, functions, and propositional proof systems starting from first principles.
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 correctness of definitions and proofs can be checked automatically. Reasoning in computational type theory is intuitionistic reasoning with optional assumptions such as excluded middle and extensionality.
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 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.
The things you learn in the course are essential for programming languages, software verification, and mathematical practice.
Students taking the course should be familiar with mathematical reasoning and functional programming. At Saarland University, we are teaching the course since 2010.
See the timetable for the dates of lectures, tutorials and office hours.
Textbook
The course follows 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 may be given in the office hours.
Lectures
Lectures are on Wednesday (12.15 - 13.45) and on Friday (12.15 - 13.45) from April 9 to July 18. Lectures take place in HS 002 in Building E1 3.
Tutorials
There are weekly tutorials where you discuss the exercise assignment with the tutor and fellow students. The tutorials are on Tuesdays at 14.15 - 15.45 and 16.15 - 17.45 in SR 016 in Building E1 3, with the first tutorial on April 16. You will be able to indicate your preferences during registration. The tutors are Lara Engelkamp and Haoyi Zeng.
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.30 - 16.30) and Thursdays (15.00 - 16.00). Starting with the second week, the office hours are in Room 525 in Building E1 3.
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 being released in the first week.
Tests
Starting with the second 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.
Exams
There will be oral exams after the lecture period determining your grade. Each participant will be assigned a 30 minutes slot. Examination slots will be available in the week August 18-22 and September 8-12 (re-exam). Details are on the exams page.
Registration
To take the course, you need to register with the CMS (see menu at the top). Registration is open April 9-13. 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.