Logical Verification 2022–2023

vu.study.guide

lean

lean.forward

Course_Data

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

Course_Objective

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

Lecturers

Teaching_Assistants

Schedule

Lecture 1 
Tuesday 15:30–17:00, weeks 44–50, room VU HG-08A33
Exercise 1
Wednesday 15:30–17:00, weeks 44–50, room VU NU-3B19
Lecture 2 
Wednesday 17:30–19:00, weeks 44–50, room VU WN-M129
Exercise 2
Friday 15:30–17:00, weeks 44–50, room VU NU-5B21
Final exam
Tuesday 20 December (week 51) 08:30–11:15 (with extra time: 11:45), rooms VU WN-S623 S631 S655
Resit exam (DRAFT)
Tuesday 14 February (week 7) 18:45–21:30 (with extra time: 22:00), rooms VU NU-3B19

See also the official VU timetable, which has precedence.

Essential_Materials

Detailed_Content

The course consists 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. Guest lecture by Heather Macbeth

Lecture_Videos

These are the videos of the lectures from 2020, covering the same material as this year. The headings and numbers correspond to the Hitchhiker's Guide. Although videos are available, we recommend that you attend the lectures.

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

Contact_information

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 practical work or technical issues with installing or running Lean, please email the teaching assistants (Dominique Danco, Sam van Kampen, and Wolf bij 't Vuur) with [LoVe] in the subject line.

For queries concerning the lectures, please email the main lecturer (Jasmin Blanchette) with [LoVe] in the subject line. Addressing an email in academia is always a puzzle; here, a simple "Dear Jasmin" 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.

Overview_of_the_Course

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.

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.

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 correspond

  1. a chapter in The Hitchhiker's Guide
  2. a Lean demo file (e.g., love01_definitions_and_statements_demo.lean)
  3. a Lean exercise sheet (e.g., love01_definitions_and_statements_exercise_sheet.lean)
  4. a Lean homework sheet (e.g., love01_definitions_and_statements_homework_sheet.lean–for the first 11 lectures only)

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, its mathematical library, and Visual Studio Code).

Lecture 14 is a special guest lecture, showing a real application of Lean.

For the group exercises, we strongly recommend that you bring your own wine^H^H^H^Hlaptop.

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. Each sheet gives 10 point (excluding bonuses). You need to collect at least 50 points to get a perfect score on the homework. Thus, you can obtain a perfect score by doing only five assignments, if you score 10 points on each.

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.

Optional_Formalization_Project

Optionally, you can choose to replace two homework sheets by a project, worth up to 20 points. 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:

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

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.

Installation instructions

Final_Exam

The final exam is on paper, closed book.

Below you will find exams from previous years as well as a mock exam.

  1. Logical Verification 2021–2022 at VU:
    final exam sheet and solution
    resit exam sheet and solution
  2. Logical Verification 2020–2021 at VU:
    final exam sheet
    resit exam sheet
  3. Logical Verification 2019–2020 at VU:
    final exam sheet and solution
    resit exam sheet and solution
  4. Logical Verification 2018–2019 at VU:
    mock exam sheet and solution
    final exam sheet
    resit exam sheet

Optional_Further_References