Logical Verification 2020–2021

vu.study.guide

lean

lean.forward

Data

MSc-level course at Vrije Universiteit Amsterdam, computer science
6 credits
Academic year 2020–2021, period 2

Objective

This courses introduces the proof assistant Lean, its type-theoretic foundations, and its applications to mathematics and computer science.

Overview

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.

Lecturers

Teaching Assistant

Schedule

See the official rooster.

Format of the course

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

  1. a Lean demo file (e.g., love01_definitions_and_statements_demo.lean)
  2. a Lean exercise sheet (e.g., love01_definitions_and_statements_exercise_sheet.lean)
  3. 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.

Detailed content

The course will consist of 14 lectures:

  1. Basics
    1. Definitions and Statements
    2. Backward Proofs
    3. Forward Proofs
  2. Functional–Logic Programming
    1. Functional Programming
    2. Inductive Predicates
    3. Monads
    4. Metaprogramming
  3. Program Semantics
    1. Operational Semantics
    2. Hoare Logic
    3. Denotational Semantics
  4. Mathematics
    1. Logical Foundations of Mathematics
    2. Basic Mathematical Structures
    3. Rationals and Real Numbers
    4. p-Adic Numbers (paper)

Materials

Installation instructions

Old exams

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

  1. Logical Verification 2019–2020 at VU (by J.C. Blanchette and A. Bentkamp):
    final exam sheet, resit exam sheet
  2. 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
  3. Logical Verification 2016–2017 at VU (by J.C. Blanchette):
    final exam, resit exam

Useful links