MSc-level course at Vrije Universiteit Amsterdam, computer science
Academic year 2020–2021, period 2
This course introduces the proof assistant Lean, its type-theoretic foundations, and its applications to mathematics and computer science.
The headings and numbers correspond to the Hitchhiker's Guide.
Lecture 1: Preface + Definitions and Statements
Lecture 2: Backward Proofs
Lecture 3: Forward Proofs
Lecture 4: Functional Programming
Lecture 5: Inductive Predicates
Lecture 6: Monads
Lecture 7: Metaprogramming
Lecture 8: Operational Semantics
Lecture 9: Hoare Logic
Lecture 10: Denotational Semantics
Lecture 11: Logical Foundations of Mathematics
Lecture 12: Basic Mathematical Structures
Lecture 13: Rational and Real Numbers
Guest Lecture: p-adic Numbers (slides)
We are available if you need help or advice, or just want to let us know about your progress or have suggestions to improve the course (for this year or next year).
For queries concerning the lectures, please email the lecturers (Jasmin Blanchette and Gabriel Ebner) with [LoVe] in the subject line. Addressing an email in academia is always a puzzle; here, a simple "Dear Jasmin" or "Dear Gabriel" suffices.
We will also try to monitor Canvas regularly, but because of the subtle blue-on-blue "You got mail" indicator, it is all too easy to miss messages there. To reach fellow students and instructors all at once, you can use Canvas for discussions and questions related to Lean. We strongly encourage this, especially in conjunction with remote learning.
Proof assistants are software tools that can be used to check the correctness of a specification of a program or the proof of a mathematical theorem. The course is concerned with Lean, a proof assistant 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.
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.
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 (The Hitchhiker's Guide to Logical Verification).
To each of the first 13 lectures 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; the "Discussions" panel of Canvas is a great way to get help and to connect with fellow students, especially in the time of cholera. We will also help you set up Lean and Visual Studio Code on your computer. See the installation instructions for the necessary software (Lean and its mathematical library).
Lecture 14 is a special guest lecture, showing a real application of Lean.
The homework given at lecture n must be submitted on Canvas by the beginning of lecture n + 2. The deadline is strict. There are 11 homework sheets, but we will only grade the first 10 that have been submitted. Thus, missing a single deadline will not affect your grade.
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.
Optionally, you can choose to replace two homeworks by a project. This is a great way to improve your theorem proving skills in little time. You can think up a nice formalization project for yourself, such as these:
You are encouraged to discuss your plans with your instructors before starting your project. You should set yourself a time limit before starting your project. Also incomplete formalizations are welcome. We will be generous while grading them, so that you are not penalized for choosing the project over the regular homework. Please document your formalization well, such that we can see what it does or is intended to do. In our experience, doing a project is the absolute best way to learn theorem proving.
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 previous exams.
Please fill out this evaluation form at the end of the course. Your feedback will greatly help improve the course.