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 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.
See the timetable for the dates of lectures, tutorials and office hours.
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
Lectures are on Wednesday (12.15 - 13.45) and on Friday (12.15 - 13.45) from April 12 to July 19. Lectures will 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 10.15 - 11.45 in SR 014 and 14.15 - 15.45 in SR 016 (both in Building E1 3), with the first tutorial on April 18. You will be able to indicate your preferences during registration. The tutors are Niklas Mück 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 an oral exam after the lecture period determining your grade. Each participant will be assigned a 30 minutes slot. There will be a re-exam in case you want to take the exam latter or you want to improve your grade. 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 3-16. 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.