Typsysteme helfen Programmierern, Eigenschaften von Programmen über alle Ausführungen des Programms hinweg sicherzustellen. Je ausdrucksstärker das Typsystem ist, desto mehr Eigenschaften lassen sich auf diese Weise abdecken. Eine besonders ausdrucksstarke Klasse von Typsystemen sind solche mit abhängigen Typen. Bei diesen kann der Typ von Programmen von konkreten Laufzeitwerten abhängen. Das Programmieren in solchen Programmiersprachen erfordert theoretisches Wissen und vor allem praktische Erfahrung. Beides wird in diesem Praktikum vermittelt.

Vorbereitung

Es ist unbedingt erforderlich Zugriff auf das Buch “Type-driven development with Idris” zu haben. Dies ist über die Bibliothek möglich.

Desweiteren ist es erforderlich eine Entwicklungsumgebung für die Programmiersprache “Idris 2” zu installieren. Visual Studio Code hat eine entsprechende Erweiterung.

Termin

Wir treffen uns ab dem 31.10.23 jede Woche dienstags um 18:00 (s.t.) in C215 auf Sand.

Ablauf

Jeweils ein Teilnehmer präsentiert ein Kapitel aus dem Buch “Type-driven development with Idris” im Stil einer Vorlesung (z.B. Informatik 1). Insbesondere auch einige der Aufgaben. Alle Teilnehmer haben das jeweilige Kapitel gelesen. Über die vorlesungsfreie Zeit programmiert jeder Teilnehmer ein Abschlussprojekt und reicht bis zum Ende des Semesters den Code und eine kurze Dokumentation ein. Die Note setzt sich zu gleichen Teilen aus der Präsentation und dem Projekt zusammen.

Abschlussprojekt

Die Einreichung des Abschlussprojekts erfolgt bis zum 29. März 2024, entweder als Archiv per Email, oder als Link zu einem Repository. In jede Fall sollte sie eine kurze Beschreibung des Projektes enthalten und eine Anleitung wie man es laufen lässt.

People

• Jonathan Brachthäuser
  Head of the SE research groupJonathan Immanuel Brachthäuser
• Philipp Schuster
  ResearcherPhilipp Schuster