Logical Verification 2019–2020

vu.study.guide

lean

lean.forward

Data

MSc-level course at Vrije Universiteit Amsterdam, computer science
6 credits
Academic year 2019–2020, 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–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.

Lecturers

Teaching Assistant

Schedule

In case of discrepancies, the official rooster has priority.

Period     
2
Lecture 1  
Monday 15:30–17:15, week 44, VU WN-F647
Monday 15:30–17:15, weeks 45, 47, and 48, VU HG-02A33
Monday 15:30–17:15, week 46, VU WN-F123
Monday 15:30–17:15, weeks 49 and 50, VU WM-M129
Exercise 1 
Tuesday 11:00–12:45, weeks 44–50, VU WN-P337 (extra: WN-P447)
Lecture 2  
Thursday 13:30–15:15, weeks 44–50, VU WN-M129
Exercise 2 
Friday 13:30–15:15, weeks 44–50, VU WN-P337 (extra: WN-P447)
Final exam 
Tuesday 15:15–18:00, week 51, room VU IN-3B39 IN-3B45 IN-3B59
Repeat exam
TBA

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 both lecturers (J.C. Blanchette and A. Bentkamp), with [LoVe] in the subject line. We will 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.

To each lecture (on Mondays and Thursdays) corresponds some notes in Markdown format (e.g., love01_definitions_and_lemma_statements.md), a Lean demo file (e.g., love01_definitions_and_lemma_statements_demo.lean), a Lean exercise sheet (e.g., love01_definitions_and_lemma_statements_exercise_sheet.lean) and a Lean homework sheet (e.g., love01_definitions_and_lemma_statements_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.

The homework given at lecture n is due by noon of the day of lecture n + 3. The homework counts for 25% of the final grade.

Detailed content

The course will consist of 14 lectures:

  1. Basics
    1. Definitions and Lemma Statements
    2. Tactical Proofs
    3. Structured Proofs and Proof Terms
  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

Material

Installation instructions

Old exams

This year's course is the second 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 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 pre-2018 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 covered Isabelle/HOL and language semantics, going well beyond what we achieve in part IV of the current course.

  1. Logical Verification 2018–2019 at VU (by J.C. Blanchette and J. Hölzl):
    mock exam sheet, mock exam solution, final exam sheet, repeat exam sheet
  2. Logical Verification 2016–2017 at VU (by J.C. Blanchette):
    final exam, repeat exam
  3. Logical Verification 2014–2015 at VU (by F. van Raamsdonk):
    repeat exam
  4. Concrete Semantics with Isabelle/HOL 2015 at UdS (by J.C. Blanchette, D. Wand, and M. Fleury):
    final exam

Useful links