Schriftliche oder mündliche Prüfung. Die Teilnahme an Übungen ist Voraussetzung für die Prüfungsteilnahme.

Dieser Kurs ist eine Einführung in die interaktive Theorem-Programmierung und fortgeschrittene funktionale Programmierung, hauptsächlich unter Verwendung des Coq-Beweisassistenten. Dieser Kurs richtet sich an Studenten, die interessiert sind an:
1. Die grundlegenden Theorien der Mathematik, vor allem Typentheorie und Logik
2. Praktisches interaktives Beweisen von Theoremen mit einem modernen Beweisassistenten
3. Fortgeschrittene funktionale Programmiersprachen und ihre Beziehung zur konstruktiven Mathematik über den "Curry-Howard-Isomorphismus"
4. Programmverifikation und "zertifizierte Programmierung"
5. Semantik von Programmiersprachen

Die Studierenden sind in der Lage, Programme zu schreiben und Theoreme mit dem Coq-Beweisassistenten zu beweisen. Die Studierenden verstehen die theoretischen Grundlagen von interaktiven Theorembeweisern und erhalten einen grundlegenden Einblick in die Semantik und die formalen Eigenschaften von Programmiersprachen.

Volume 1 and 2 of the “Software Foundations” series available at https://softwarefoundations.cis.upenn.edu/.
A. Chlipala, Certified Programming with Dependent Types, MIT Press / A background in functional programming is helpful. Experience with mathematical proofs is helpful.