Admission requirements
There are no admission requirements, although following Computational Modelsand Semantics (4343CMS6X) first is recommended.
Description
A formal proof of a theorem starts from a given set of premises, and then applies logically sound rules to reach the desired conclusion. It is typically understood that such a proof could, in principle, be mechanically checked by a machine, to see if no extra assumptions were made, and each of the rules was applied correctly. Proofs encountered in the literature, on the other hand, are usually rendered in natural language. This increases the risk of human error — perhaps an induction hypothesis was applied incorrectly, the author forgot to cover a certain case, or some additional assumption was made inadvertently.
Proof assistants help bridge this gap, by providing the user with a rigorous, machine-checked language to encode their assumptions, claims, and proofs. Modern proof assistants are general and flexible enough to express complicated arguments. They can also help to automate the "boring parts" of an argument, allowing the user to focus on steps that require creativity.
In this course, you will learn how to use the Coq proof assistant. We will start by gaining a basic familiarity with Coq itself, discussing how common mathematical formalisms can be encoded, and how you can write proofs interactively. Although Coq can and is used for general mathematics, we will emphasize use cases in computer science in the examples an exercises, with a particular focus on applications to programming language semantics.
The course will consist of lectures, complemented by exercise sessions and practical assignments. The course will conclude with an individual project, in which you will propose and formalize a topic of your choosing.
Course objectives
In this course, you will learn how to
encode common proof methods and mathematical models in Coq
automate formal proofs using built-in decision procedures
write your own tactic scripts to simplify proofs
formalize aspects of programming language semantics
apply dependent types to guarantee certain program properties
deal with the limitations imposed by a strong type system
leverage the Curry-Howard isomorphism to your advantage
Timetable
The most recent timetable can be found at the Computer Science (MSc) student website.
In MyTimetable, you can find all course and programme schedules, allowing you to create your personal timetable. Activities for which you have enrolled via MyStudyMap will automatically appear in your timetable.
Additionally, you can easily link MyTimetable to a calendar app on your phone, and schedule changes will be automatically updated in your calendar. You can also choose to receive email notifications about schedule changes. You can enable notifications in Settings after logging in.
Questions? Watch the video, read the instructions, or contact the ISSC helpdesk.
Note: Joint Degree students from Leiden/Delft need to combine information from both the Leiden and Delft MyTimetables to see a complete schedule. This video explains how to do it.
Mode of instruction
The course consists of lectures, workgroups, programming assignments in pairs, and an individual project concluded with a report and presentation.
Course load: 168h total, divided as follows:
Lectures: 20h
Workgroups: 20h
Assignments: 40h
Course project: 60h
Final report: 20h
Presentations: 8h
Assessment method
The final grade is calculated as follows:
Assignments: 30% (group grade)
Course project and report: 60% (individual)
Final presentation: 10% (individual)
To pass this course, a passing grade for the course project is required.
There is one statutory resit opportunity for the course project, but not for the other components. This resit amounts to a second deadline for the course project. Addressing all feedback received on a possible first attempt at the course project does not guarantee a perfect grade on the resit.
Reading list
During the course, we will use selected material from the following books, which are freely available online:
Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, and Brent Yorgey: Logical Foundations (Software Foundations, Vol. 1) https://softwarefoundations.cis.upenn.edu/lf-current/index.html
Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, Brent Yorgey: Programming Language Foundations (Software Foundations, Vol. 1) https://softwarefoundations.cis.upenn.edu/plf-current/index.html
Registration
As a student, you are responsible for enrolling on time through MyStudyMap.
In this short video, you can see step-by-step how to enrol for courses in MyStudyMap.
Extensive information about the operation of MyStudyMap can be found here.
There are two enrolment periods per year:
Enrolment for the fall opens in July
Enrolment for the spring opens in December
See this page for more information about deadlines and enrolling for courses and exams.
Note:
It is mandatory to enrol for all activities of a course that you are going to follow.
Your enrolment is only complete when you submit your course planning in the ‘Ready for enrolment’ tab by clicking ‘Send’.
Not being enrolled for an exam/resit means that you are not allowed to participate in the exam/resit.
Contact
All course material will be available on the course website. Grades and course updates will be communicated through Brightspace.
Remarks
Software
Starting from the 2024/2025 academic year, the Faculty of Science will use the software distribution platform Academic Software. Through this platform, you can access the software needed for specific courses in your studies. For some software, your laptop must meet certain system requirements, which will be specified with the software. It is important to install the software before the start of the course. More information about the laptop requirements can be found on the student website.