MSc-level course at Vrije Universiteit Amsterdam, computer science
Academic year 2020–2021, period 2
This courses introduces the proof assistant Lean, its type-theoretic foundations, and its applications to mathematics and computer science.
A proof assistant is used to check the correctness of a specification of a program or the proof of a mathematical theorem. The course is concerned with the proof assistant Lean, a system that is developed primarily at Microsoft Research. In the practical work, we learn to use Lean. We will see how to use the system to prove mathematical theorems in a precise, formal way, and how to verify small functional programs (e.g., a sorting algorithm). In the course, we focus on its dependent type theory and on the Curry–Howard correspondence between proofs and functional programs (λ-terms). These concepts are the basis of Lean but also of other popular systems, including Agda, Coq, and Matita.
See the official rooster.
The course is oriented towards the application of proof assistants to computer science and mathematics. We will use Lean, a modern system developed at Microsoft Research. In each lecture, we will review a Lean file, which can be downloaded from the materials section below.
If you need to contact us, please email the lecturer (J.C. Blanchette) or the teaching assistant (V.V.V. Nummelin) with [LoVe] in the subject line. A simple "Dear Jasmin" or "Dear Visa" suffices. We will also monitor Canvas regularly. You can use Canvas for discussions and questions related to Lean.
Although the course is application-driven, this is a university course, so theory is important as well. We will cover it as it emerges, but you are expected to read the materials we refer to, especially the lecture notes.
To each lecture corresponds
The exercises are crucial. Theorem proving can only be learned by doing. We will assist you during the group exercises and answer questions on Canvas. We will also help you set up Lean and Visual Studio Code on your computer. See below for links to software and installation instructions.
For the group exercises, we strongly recommend that you bring your own wine^H^H^H^Hlaptop.
The homework given at lecture n is due by the beginning of lecture n + 2. The homework counts for 25% of the final grade and must therefore be done individually. As in previous years, suspected cases of plagiarism will be reported to the examination board.
The course will consist of 14 lectures:
This year's course is the third of its kind, with the emphasis on practical applications and on dependent type theory in Lean. Below you will find a mock exam as well as some exams from previous years