Overview  Organization  Schedule  Chat  Material 
Interactive Theorem Proving (ITP)
Lecture 2 hours, Blanchette; exercises 2 hours, Généreux, Toth
Recognized as “Fortgeschrittene Themen der theoretischen Informatik” and “Vertiefende Themen der Informatik”.
Overview
This course introduces the proof assistant Lean 4, its typetheoretic 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

2+2 hours per week

Lecturer: Prof. Dr. Jasmin Blanchette

Teaching assistants: Xavier Généreux, Balazs Toth
Place and Time
Activity  Time  Place  Start 

Lecture  Wed 1416  Amalienstr. 73a, room 112  17.04.2024 
Group exercise  Thu 1214  GSP F 007  18.04.2024 
For the group exercises, we strongly recommend that you bring your own laptop with Lean 4 installed on it.
Schedule
The course consists of the following 14 lectures:
Basics:
1. Types and Terms
2. Programs and Theorems
3. Backward Proofs
4. Forward Proofs
Functional—Logic Programming:
5. Functional Programming
6. Inductive Predicates
7. Effectful Programming
8. Metaprogramming
Program Semantics:
9. Operational Semantics
10. Hoare Logic
11. Denotational Semantics
Mathematics:
12. Logical Foundations of Mathematics
13. Basic Mathematical Structures
14. Rationals and Real Numbers
The second half of lecture 13 will be a guest lecture.
The second half of lecture 14 will be reserved for revision as well as questions and answers.
Chat
There is a Zulip chat room associated with the lecture where you can ask organizational and contentrelated questions. Please use it if possible, instead of sending us emails, so that your fellow students can also benefit from the answers.
ZulipServer: https://chat.ifi.lmu.de
Stream: TCS24SITP
Material

The Hitchhiker’s Guide to Logical Verification (desktop edition)

The Hitchhiker’s Guide to Logical Verification (tablet edition)
In each lecture, we will review a Lean file, which can be downloaded from the git repository.
To each of the 14 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 12 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.
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 Instructions
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.
Final Exam
The course aims at teaching concepts, not syntax. Therefore, the final exam is on paper. It is also closed book.
The exam will take place on Thursday 25.07.2024 from 16:00 in Theresienstr. 39 B 138. You will be given 120 minutes to complete it.
If you need some adjustments to compensate for disabilities or impairments, please contact the lecturer well before the exam.
Artikelaktionen