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.

Ablauf

Wir treffen uns jede Woche. Der Wochentag, die Uhrzeit, und der Raum werden noch hier bekannt gegeben.

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.

People

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