Jonathan Weinberger (Chapman University) will join us for a talk on current developments in program verification and type theory. This will be interesting for anyone who has been astounded by recent progress in proof assistants and automated mathematics.
The talk will take place in Room Berkeley/Shanghai (HLRS) at August 11th, 15:00. Should you want to attend in person, please write to nico.formanek@hlrs.de.
We will also stream the talk online at webex: https://unistuttgart.webex.com/unistuttgart/j.php?MTID=me2b9427f270cf54df7c4e163a4aee661
Abstract:
A crucial way to ensure correctness of programs is through working with the correct data types. I will give an overview on how type theory can be used as a foundation for logic and mathematics, and how it can be used as a programming language for higher-dimensional structures, such as spaces studied in geometry and topology. This leads to the program of homotopy type theory (HoTT) and univalent foundations, pioneered by Fields medalist Vladimir Voevodsky. As opposed to „analytical mathematics“ where complex objects are built from unstructured sets from the ground up we will give examples of „synthetic mathematics“ where the highly structured objects are themselves primitive. As an example I will present recent a formalization project (joint work with Nikolai Kudasov and Emily Riehl) and further advances (joint work with Daniel Gratzer and Ulrik Buchholtz) in the area of synthetic higher category theory.