Admission requirements
There are no formal admission requirements, although following Computational Models and Semantics (4343CMS6X) first is recommended.
Students without prior knowledge of functional programming languages (e.g., Haskell) will have to catch up on some intuition, but this should not be an insurmountable obstacle.
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 Rocq Prover. We will start by gaining a basic familiarity with Rocq itself, discussing how common mathematical formalisms can be encoded, and how you can write proofs interactively. Although Rocq can be used for general mathematics, we will emphasize use cases in computer science in the examples an exercises, with a particular focus on applications to (functional) algorithm verification and 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 Rocq
automate formal proofs using built-in decision procedures
use tacticals and other techniques to simplify proof scripts
deal with the limitations imposed by a strong type system
leverage the Curry-Howard isomorphism to your advantage
formalize aspects of programming language semantics
apply dependent types to guarantee certain program properties
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 presentation.
Course load: 168h total, divided as follows:
Lectures: 24h
Workgroups: 24h
Assignments: 40h
Course project: 70h
Presentations: 10h
Assessment method
This course has an attendance requirement of 75% of all lectures and workgroups. Students who do not meet this requirement will be unable to pass this course unless extenuating circumstances apply.
The final grade is calculated as follows:
Assignments: 30% (group grade)
Course project: 60% (individual)
Final presentation: 10% (individual)
To pass this course, a sufficient grade (5.5 or higher) for the course project is required. Furthermore, before starting the course project, students are required to hand in a project proposal, where they discuss the objectives of their course project in detail.
There is one statutory resit opportunity for the course project and the accompanying final presentation, but not for the other components. This resit amounts to a second deadline for the course project, and a second attempt at the final presentation. 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 can be used free of charge
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). Available online.
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. 2). Available online.
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, grades, and updates will be available through Brightspace.
Remarks
Software
As mentioned above, we will be using the Rocq Prover, which is available free of charge for a range of different platforms. Installation should be easy, although instructions will be provided.