Funktionale Programmierung in Lean PI5515
Lean ⇗ ist eine funktionale Sprache und ein interaktives Beweissystem.
Als funktionale Sprache bevorzugt man in Lean reine Funktionen, deren Returnwert einzig und allein von den übergebenen Argumenten abhängt. Solche Funktionen haben keine Seiteneffekte und eignen sich deshalb insbesondere in nebenläufigen Situationen. In Lean hat jeder Ausdruck einen Typ und der Typchecker von Lean kann solche Typen prüfen, sogar dann, wenn sie von Werten abhängen (dependent types).
Das Besondere an Lean besteht darin, dass wir nicht nur funktionale Programme implementieren können, sondern dass man auch ihre Eigenschaften spezifizieren und beweisen kann — und dies in der Sprache Lean selbst! Denn das interaktive Beweissytem von Lean beruht auf der Typüberprüfung der Sprache.
In diesem Kurs konzentrieren wir uns auf Lean als funktionale Sprache, aber natürlich kommen auch Beispiele vor, die demonstrieren, wie man Eigenschaften von Funktionen mit Lean beweisen kann.
Die Vorlesung selbst ist auch interaktiv: Das Skript besteht aus Lean-Quellen, die wir in der Veranstaltung live in Visual Studio Code durchgehen. Die Teilnehmerinnen und Teilnehmer werden ermuntert, in der Vorlesung selbst den Code mitzuverfolgen und auch mit ihm zu experimentieren.
Inhalt
- Erste Begegnung mit Lean
- Datentypen definieren und verwenden
- Weitere eingebaute Typen
- Verkettete Listen und Arrays
- Ausführbare Programme erzeugen
- Typklassen
- Logische Verifikation
- Programmierung mit Effekten
- Mehr über Monaden
- Abhängige Typen
Moodle-Kurs zur Veranstaltung ⇗
Materialien
 |
Burkhardt Renz: Funktionale Programmierung in Lean. Vorlesungsskript THM, Januar 2025 Portable Document Format, 940 KB, Stand 20.01.2025 |
 |
Burkhardt Renz: Quellen des Skripts. Januar 2025 Zip Archivdatei, 88 KB, Stand 20.01.2025 |
Das Skript wird noch überarbeitet und erweitert, insbesondere in den hinteren Kapiteln.