Functional Programming in Lean
General Information
- Lecturer: Prof. Dr. Peter Thiemann
- Assistant: Marius Weidner
- Lecture: Tuesday 2PM, Building 106 Room 04 007, zoom
- Tutorial: Monday 10AM, Building 101 Room 00-017/19, zoom
- Chat: zulip channel
Lecture
| Date | Topic | Material | Recording |
|---|---|---|---|
| Tu 2026-10-20 | Introduction | Slides 01, Week01.lean | rec |
| Tu 2026-10-27 | Inductive Definitions and Pattern Matching | Slides 02-1, Slides 02-2, Week02.lean, Week03.lean | rec |
| Tu 2026-11-03 | Higher-Order Functions | Slides 03, Week04.lean | rec |
| Tu 2026-11-10 | |||
| Tu 2026-11-17 | No lecture. Join us at the talk by Joachim Breitner (Lean FRO), Lean – Architecture, Meaning and Trust, 14:30–16:00, SR 404, Mathematical Institute | - | - |
Tutorial
| Date | Topic | Material | Recording |
|---|---|---|---|
| Mo 2026-10-26 | canceled | - | - |
| Mo 2026-11-02 | Inductive Definitions and Pattern Matching | Sheet 01, Template01.lean, Solution01.lean | rec |
| Mo 2026-11-09 | Higher-Order Functions | Sheet 02, Template02.lean | - |
Exam
| Date | Time | Place | Mode |
|---|---|---|---|
| tba. | tba. | computer pools | closed block, live programming |