MSc-level course at Vrije Universiteit Amsterdam, computer science

6 credits

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.

- Jasmin Blanchette (VU Amsterdam)

- Visa Nummelin (VU Amsterdam)

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

- a Lean demo file (e.g.,
`love01_definitions_and_statements_demo.lean`) - a Lean exercise sheet (e.g.,
`love01_definitions_and_statements_exercise_sheet.lean`) - a Lean homework sheet (e.g.,
`love01_definitions_and_statements_homework_sheet.lean`)

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:

- Basics
- Definitions and Statements
- Backward Proofs
- Forward Proofs

- Functional–Logic Programming
- Functional Programming
- Inductive Predicates
- Monads
- Metaprogramming

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

- Mathematics
- Logical Foundations of Mathematics
- Basic Mathematical Structures
- Rationals and Real Numbers
*p*-Adic Numbers (paper)

- Lean and PDF files (git repository)
*The Hitchhiker's Guide to Logical Verification*(lecture notes)

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

- Logical Verification 2019–2020 at VU (by J.C. Blanchette and A. Bentkamp):

final exam sheet, resit exam sheet - Logical Verification 2018–2019 at VU (by J.C. Blanchette and J. Hölzl):

mock exam sheet, mock exam solution, final exam sheet, resit exam sheet - Logical Verification 2016–2017 at VU (by J.C. Blanchette):

final exam, resit exam

- Lean (web page)
- Visual Studio Code (web page)
- Lean's mathematical library (git repository)
*Theorem Proving in Lean*(tutorial)*Concrete Semantics: With Isabelle/HOL*(book)