Links und Funktionen
Inhaltsbereich

Interactive Theorem Proving (ITP)

Lecture 2 hours, Blanchette; exercises 2 hours, Généreux, Xu

Recognized as “Fortgeschrittene Themen der theoretischen Informatik” and “Vertiefende Themen der Informatik” in the Bachelor and the Master. For BSc students, the course is officially called “Interactive Theorem Proving for Bachelor”.

Overview

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

Proof assistants are pieces of software that can be used to check the correctness of a specification of a program or the proof of a mathematical theorem. 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. In the course, we focus on Lean’s 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.

There are no formal prerequisites, but familiarity with functional programming (e.g., Haskell) and basic algebra is an asset. If you are new to functional programming, we recommend that you read the first chapters of Learn You a Haskell for Great Good!, stopping at the section “Only folds and horses”.

Organization

Schedule

The course consists of the following 13 regular lectures:

Basics:

Lecture 1. Types and Terms
Lecture 2. Programs and Theorems
Lecture 3. Backward Proofs
Lecture 4. Forward Proofs

Functional—Logic Programming:

Lecture 5. Functional Programming
Lecture 6. Inductive Predicates
Lecture 7. Effectful Programming
Lecture 8. Metaprogramming

Program Semantics:

Lecture 9. Operational Semantics
Lecture 10. Hoare Logic

Mathematics:

Lecture 11. Logical Foundations of Mathematics ()
Lecture 12. Basic Mathematical Structures ()
Lecture 13. Rational and Real Numbers (*)

Lecture 14 will be a guest lecture followed by revision for the exam, including questions and answers.

Lectures marked with a star (*) present material that is relevant for the exam for MSc students but not for BSc students.

Chat

There is a Zulip chat room associated with the lecture where you can ask organizational and content-related questions. Please use it if possible, instead of sending us emails, so that your fellow students can also benefit from the answers.

Zulip-Server: https://chat.ifi.lmu.de
Stream: TCS-25S-ITP

Material

In each lecture, we will review a Lean file, which can be downloaded from the git repository.

To each of the lectures correspond

  • a chapter in The Hitchhiker’s Guide to Logical Verification

  • a Lean demo file (e.g., LoVe01_TypesAndTerms_Demo.lean)

  • a Lean exercise sheet (e.g., LoVe01_TypesAndTerms_ExerciseSheet.lean)

and for the first 11 lectures

  • a Lean homework sheet (e.g., LoVe01_TypesAndTerms_HomeworkSheet.lean)

The Hitchhiker’s Guide consists of a preface and 14 chapters. They cover the same material as the corresponding lectures but with more details. Chapter 11, about denotational semantic, is not relevant for the exam.

The exercises are crucial. Theorem proving can only be learned by doing. We will assist you during the group exercises and answer questions on Zulip. We will also help you set up Lean and Visual Studio Code on your computer. After each tutorial, the solutions of the weekly exercices will be made available in the git repository for reference.

The homework is optional but highly recommended. The solution of each homework will be made available in the git repository at the beginning of the following week’s lecture.

Installation

To install Lean, follow the official installation instructions.

To edit the Lean files associated with this course, open the lean folder as a Lean 4 project as described here.

Exams

The course aims at teaching concepts, not syntax. Therefore, the exams are on paper. They are also closed book. You will be given 120 minutes to answer.

If you need some adjustments to compensate for disabilities or impairments, please contact the lecturer well before the exam.

Past Year Exams

Interactive Theorem Proving SoSe 2024:

This year’s course is based roughly on the same material as the course Logical Verification at the Vrije Universiteit Amsterdam. Exams from previous years are available below. Note that they use Lean 3 syntax.

Logical Verification 2022—2023:

Logical Verification 2021—2022:

Logical Verification 2020—2021:

Logical Verification 2019—2020:

Logical Verification 2018—2019:

Artikelaktionen

Funktionsleiste