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.
You will find the timetables for all courses and degree programmes of Leiden University in the tool MyTimetable (login). Any teaching activities that you have sucessfully registered for in MyStudyMap will automatically be displayed in MyTimeTable. Any timetables that you add manually, will be saved and automatically displayed the next time you sign in.
MyTimetable allows you to integrate your timetable with your calendar apps such as Outlook, Google Calendar, Apple Calendar and other calendar apps on your smartphone. Any timetable changes will be automatically synced with your calendar. If you wish, you can also receive an email notification of the change. You can turn notifications on in ‘Settings’ (after login).
For more information, watch the video or go the the 'help-page' in MyTimetable. Please note: Joint Degree students Leiden/Delft have to merge their two different timetables into one. This video explains how to do this.
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
From the academic year 2022-2023 on every student has to register for courses with the new enrollment tool MyStudyMap. There are two registration periods per year: registration for the fall semester opens in July and registration for the spring semester opens in December. Please see this page for more information.
Please note that it is compulsory register your participation for every exam and retake. Not being registered for a course means that you are not allowed to participate in the final exam of the course.
Extensive FAQ's on MyStudymap can be found here.
Contact
All course material will be available on the course website. Grades and course updates will be communicated through Brightspace.
Remarks
None.