??? + Lambda-Pi-Kalkül

Michael Färber ist bei uns zu Gast und wird über Beweisüberprüfung mittels des Lambda-Pi-Kalküls vortragen:

Der Lambda-Pi-Kalkül modulo Termersetzung erlaubt es, auf elegante Art verschiedene logische Systeme zu formalisieren und Beweise aus diesen Systemen einheitlich zu überprüfen.

Ich präsentiere zuerst den Lambda-Pi-Kalkül und zeige dann, wie man höherstufige Logik in diesem Kalkül formalisiert. Anschließend zeige ich ein Zwischenergebnis meiner Zusammenarbeit mit Makarius, nämlich einen Export von Isabelle in den Lambda-Pi-Kalkül. Abschließend präsentiere ich meine minimalistische Implementierung eines Typenprüfers für den Lambda-Pi-Kalkül.

Zusätzlich wird es Fortsetzungen der Vorträge vom letzten Mal geben.