Programm für das sechzehnte Treffen am 14. Juli 2016

Makarius stellte Cobra vor, ein modernes Framework, um Code und Beweise zu präsentieren. Cobra unterstützt Isabelle-Beweise sowie Scala- und Haskell-Code.

Ingo begann unter dem Titel Was sind und was sollen die Typen? eine Einführung in Typtheorie unter besonderer Beachtung von Homotopietyptheorie. Die grundlegende Motivation aus der Informatik und der Programmierpraxis sind natürlich bekannt: Man möchte zur Compilezeit Informationen über das Programmverhalten gewinnen, um fehlerhafte Programme noch vor ihrer Ausführung erkennen und ablehnen zu können.

Aber es ist vielleicht weniger bekannt, wie Typtheorie entstanden ist (das war nämlich lange vor den Programmiersprachen), welches Problem sie ursprünglich lösen sollte (und auch tatsächlich löst), und wie ein Typsystem aufgebaut ist.

Ziel des ersten Teils war, ein Grundverständnis im Lesen von Typsystemspezifikationen zu vermitteln. Es wurde extensionale und intensionale Martin-Löf-Typtheorie behandelt.

Homotopietyptheorie ist ein neuer Zweig der Mathematik, der Aspekte von verschiedenen anderen Teilgebieten der Mathematik auf verblüffende Art und Weise kombiniert. Es ist Teil von Voevoedskys Programm zu einer univalenten Grundlegung der Mathematik und basiert auf einer kürzlich entdeckten Verbindung zwischen Homotopietheorie aus der Mathematik und Typtheorie aus der Logik und theoretischen Informatik.

In gewöhnlichen Zugängen zu einer Grundlegung der Mathematik unterscheidet man zwischen Objekten (wie zum Beispiel natürlichen Zahlen und Mengen) und Aussagen über diese Objekte. In Homotopietyptheorie gibt es diese Unterscheidung nicht. Objekte und Aussagen über Objekte werden auf eine gemeinsame Stufe gestellt. Beweisen und Konstruieren werden miteinander identifiziert.

Der Vortrag setzt keine Vorkenntnisse aus Logik und Typtheorie und selbstverständlich auch keine aus Homotopietheorie voraus. Der Vortrag ist für Leute konzipiert, die sich für diese neue Bewegung in der Logik interessieren, aber nicht praktizierende Mathematikerinnen sind.

Er klärt folgende Fragen: Was hat es mit Homotopietyptheorie auf sich? Wie werden in Homotopietyptheorie Objekte und Aussagen miteinander vereint, auf eine Stufe gestellt? Wozu ist Homotopietyptheorie gut? Wieso und für wen ist sie interessant?

Ein Teil der Antwort auf die letzte Frage lautet: Homotopietyptheorie ist für Leute interessant, die computergestützt Beweise führen möchten.