• Prof. Dr. Burkhardt Renz

• Prof. Dr. Burkhardt Renz

Keine

INF2517 Funktionale Programmierung

Das Modul vermittelt funktionale Programmierung in Lean. Die Studierenden lernen nicht nur die funktionale Sprache Lean kennen, sondern auch wie man in Lean selbst die Korrektheit von Programmen beweisen kann.

• Erste Begegnung mit Lean
• Datentypen definieren und verwenden
• Algebraische Datentypen
• Ausführbare Programme erzeugen
• Generischer Polymorphismus und Typklassen
• Beweise der Korrektheit von Programmen
• Programmierung von Effekten mit Monaden
• Abhängige Typen und Logik

Fachkompetenzen

• Die Studierenden sind in der Lage, sowohl grundlegende als auch fortgeschrittene Konzepte der funktionalen Programmierung in Lean für konkrete Fragestellungen anzuwenden.
• Sie sind in der Lage, die Konzepte der Sprache auf neue Domänen anzuwenden.
• Sie können wichtige funktionale Muster und Abstraktionen, wie bspw. Funktoren und Monaden, erklären und auch selbst definieren und können die typischen Einsatzgebiete dieser Konzepte benennen.
• Sie können nicht nur Funktionen definieren, sondern auch ihre Eigenschaften spezifizieren und sie können Beweise führen, dass diese Eigenschaften erfüllt sind.
• Sie können Eigenschaften von Funktionen in Lean selbst spezifizieren und beweisen.
• Sie können das Terminieren von Funktionen beweisen, wenn dies erforderlich und möglich ist.

Methodenkompetenzen (fachlich & überfachlich)

• Die Studierenden können eine Fragestellung der Programmierung in ihren konkreten Details analysieren und unter Einsatz des funktionalen Paradigmas in der Sprache Lean abstrahieren und implementieren.
• Sie können komplexe strukturelle und funktionale Problemstellungen analysieren sowie Lösungen unter Zuhilfenahme des funktionalen Paradigmas synthetisieren.
• Sie können die vermittelten Lösungsstrategien auf andere Problemdomänen anwenden.

Sozialkompetenzen

• Die Studierenden können sich auf Basis ihrer theoretischen Kenntnisse eine eigene Meinung zu natur- und strukturwissenschaftlichen Problemen bilden.
• Sie können Aufgaben und Projekte in Gruppen gemeinsam konstruktiv lösen und sich dabei gegenseitig unterstützen.
• Sie können Lösungsvorschläge für fachliche Problemstellungen argumentativ sachlich vertreten.

Selbstkompetenzen

• Die Studierenden können eigenständig, selbstmotiviert und kritisch denkend Lösungsansätze für strukturelle, funktionale Problemstellungen entwickeln.
• Sie sind in der Lage, Projekte eigenständig durchzuführen und über den Projektverlauf kritisch zu reflektieren.
• Sie können Lösungen konzentriert, genau und zielgerichtet erarbeiten.

• 6 CrP
• Arbeitsaufwand 180 Std.
• Präsenzzeit 60 Std.
• Selbststudium 120 Std.

• 4 SWS
• Seminaristischer Unterricht 4 SWS

• Informatik (M.Sc. 2022)

Nein

Bonuspunkte werden gemäß § 9 (4) der Allgemeinen Bestimmungen vergeben. Art und Weise der Zusatzleistungen wird den Studierenden zu Veranstaltungsbeginn rechtzeitig und in geeigneter Art und Weise mitgeteilt.

Prüfungsvorleistung:

Keine

Prüfungsleistung:

Klausur, mündliche Prüfung oder Entwicklung in der Informatik

(Art des Leistungsnachweises wird den Studierenden rechtzeitig und in geeigneter Weise bekannt gegeben.)

• Christiansen, D. T.: Functional Programming in Lean. https://lean-lang.org/functional_programming_in_lean/)
• Lean Manual: https://docs.lean-lang.org/lean4/doc/
• Baanen, A.; Bentkamp, A.; Blanchette, J.; Hölzl, J.; Limperg, J.: The Hitchhiker's Guide to Logical Verification. https://github.com/lean-forward/logical_verification_2024/raw/main/hitchhikers_guide_2024_desktop.pdf
• Weiterführende Literatur wird im Skript des Kurses (Burkhardt Renz: Programmierung in Lean) verzeichnet.