MSc-level course at Vrije Universiteit Amsterdam, computer science

6 credits

Academic year 2018–2019, 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–De Bruijn 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.

- Jasmin Blanchette (VU Amsterdam)
- Johannes Hölzl (VU Amsterdam)

- Alexander Bentkamp (VU Amsterdam)

- Period
- 2
- Lecture 1
- Monday 15:30–17:15, weeks 44–50, VU WN-M623
- Exercise 1
- Tuesday 15:30–17:15, weeks 44–50, VU WN-P337
- Lecture 2
- Thursday 13:30–15:15, weeks 44–50, VU WN-C659
- Exercise 2
- Friday 11:00–12:45, weeks 44–50, VU WN-P337
- Exam
- Tuesday 15:15–18:00, week 51, VU WN-Q112
- Repeat exam
- Tuesday 15:15–18:00, week 5

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; for example, for the first lecture the file is called
`11_lecture.lean`. It can be downloaded from the materials section below.

If you need to contact us, please use email and write to both of us (J.C. Blanchette and J. Hölzl), with `[LV]` in the subject
line. We will try to monitor Canvas regularly. You can also 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, such
as *Theorem
Proving in Lean*.

To each lecture (on Mondays and Thursdays) corresponds some notes in Markdown format (e.g.,
`11_notes.md`), a Lean exercise sheet (e.g.,
`11_exercise_sheet.lean`) and a Lean homework sheet (e.g.,
`11_homework_sheet.lean`). The exercises are crucial; theorem
proving can only be learned by doing. We will assist you during the group
exercises (on Tuesdays and Fridays) 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. Otherwise, you can also use the online Lean interface.

The homework given at lecture *n* is due by the **beginning** of lecture
*n* + 2. The homework is mandatory for obtaining a passing grade at the
end.

We have experience teaching Isabelle/HOL and Coq, but this is the first time we teach Lean. We are open to suggestions on how to enhance the teaching materials for future years. Of course, we will be happy to help if you run into difficulties. Please do not hesitate to contact us.

Exceptionally, the homework for lectures 3.3 and 4.1 will be replaced by a project. You can think up a nice formalization project for yourself, such as these:

- Define a functional data structure (e.g., some kind of trees) and verify a few operations on it.
- Define your own small programming language and study its semantics formally.
- Formalize some results from undergrad mathematics.

You should set yourself a time limit before starting your project. Also incomplete/unfinished formalizations are welcome and will be graded. Please comment your formalization well, such that we can see what it does or is intended to do. You are welcome to discuss your plans with your instructors before starting your project.

The course will consist of 14 lectures:

- Basics
- Definitions and Propositions
- Proofs
- More Logic and Proofs

- Functional Programming
- Lists
- Trees
- Side Effects
- Custom Tactics via Metaprogramming

- Program Semantics
- Operational Semantics
- Denotational Semantics
- Hoare Logic

- Mathematics
- Foundations
- Algebra
- Rationals and Reals
- Category Theory

The above list is subject to changes.

- [ 1.1 := [Lecture Notes (Markdown), Lecture Demo, Exercise Sheet, Exercise Solution, Homework Sheet]
- 1.2 := [Lecture Notes (Markdown), Lecture Demo, Exercise Sheet, Exercise Solution, Homework Sheet]
- 1.3 := [Lecture Notes (Markdown), Lecture Demo, Exercise Sheet, Exercise Solution, Homework Sheet]
- 2.1 := [Lecture Notes (Markdown), Lecture Demo, Exercise Sheet, Exercise Solution, Homework Sheet]
- 2.2 := [Lecture Notes (Markdown), Lecture Demo, Exercise Sheet, Exercise Solution, Homework Sheet]
- 2.3 := [Lecture Notes (Markdown), Lecture Demo, Exercise Sheet, Exercise Solution, Homework Sheet]
- 2.4 := [Lecture Notes (Markdown), Lecture Demo, Exercise Sheet, Homework Sheet]

This year's course is the first of its kind, with the focus on practical applications and on dependent type theory in Lean. Below you will find some exams from previous years for related courses at the VU and the Universität des Saarlandes in Saarbrücken. These give a rough idea of what "formal proofs on paper" can look like.

Please note that the previous Logical Verification course had a stronger focus on the metatheory of dependent type theory and on the Curry–Howard correspondence (and less on practical applications), and the course in Saarbrücken used Isabelle/HOL and language semantics, going well beyond what we achieve in part 3 of the current course. Closer to the exam, we will make some dedicated practice material available.

- Logical Verification 2016–2017 at VU (by J.C. Blanchette):

final exam, repeat exam - Logical Verification 2014–2015 at VU (by F. van Raamsdonk):

repeat exam - Concrete Semantics with Isabelle/HOL 2015 at UdS (by J.C. Blanchette):

final exam

- Installing Lean (alternative instructions)
- Lean (online interface)
- Visual Studio Code
- Tutorial on
*Theorem Proving in Lean* - Lean's mathematical library (for part 4 of the course)

To participate at the exam, you must have submitted and passed all of the practical work.