Interactions of Proof Assistants and Mathematics
International Summer School, Regensburg, Germany, 2023
Important Dates
Application: May - June 9 2023In-person registration: Aug 1 2023
Online registration: Sept 15 2023
Summer school: Sept 18-29 2023
Links
Contact the Organizers
itp-school-2023@googlegroups.comLecturers at the Summer School
Note to the lecturers: we have been notified that some people were contacted by companies such as Traveller Point concerning travel arrangements. Any offers of this kind are spam and should be ignored!
Benedikt Ahrens
Benedikt Ahrens is an assistant professor at Delft University of Technology (Netherlands), and a Birmingham Fellow at University of Birmingham (UK).
Ahrens received his Ph.D. in mathematics from Université Nice Sophia Antipolis, supervised by André Hirschowitz. He was a postdoctoral researcher at the Institute for Advanced Study in 2012/13 (during the Special Year on Homotopy Type Theory and Univalent Foundations) and in 2015/16.
Jointly with others, Ahrens has been developing category theory and its applications in univalent foundations. He is a co-founder and co-maintainer of the UniMath library of computer-checked mathematics in the univalent style. Many of his research results are computer-checked in UniMath.
Ahrens is the main organizer of the School on Univalent Mathematics, which teaches students in univalent foundations and the computer-implementation of mathematics in univalent foundations.
Steve Awodey
Steve Awodey is a professor of Philosophy and Mathematics at Carnegie Mellon University.
He studied in Marburg, Germany, and at the University of Chicago,
where he did his PhD under Saunders Mac Lane.
He works on Category Theory, Logic, and Homotopy Type Theory.
Andrej Bauer
Andrej Bauer is a professor of computational mathematics at the Faculty of Mathematics and Physics of the University of Ljubljana. In 1994 he received his Sc.B. in Mathematics from Ljubljana, and in 2000 he received his PhD in Pure and Applied Logic from Carnegie Mellon University under the supervision of Dana S. Scott. In 2001, he spent a semester at the Mittag-Leffler Institute in Stockholm, Sweden. In 2012, he was a fellow at the Institute for Advanced Study, where he contributed to the development of homotopy type theory. Bauer’s work spans foundations of mathematics, constructive and computable mathematics, type theory, homotopy type theory, and mathematical principles of programming languages. He is an author of the book “Homotopy Type Theory: Univalent Foundations of Mathematics” and the initiator of the HoTT library, an extensive formalization of homotopy type theory in the Coq proof assistant. He is also known for his seminal work on programming with algebraic effects and handlers. Lately he has been working on type theory and the design of proof assistants.
Yves Bertot
Yves Bertot has been a research scientist at Inria since 1992. He specialized in proofs in type-theory, studying in turn programming language properties (with a publication at Tapsoft in 1995 with R. Fraer, Lernet Alfa Summer School 2009, Book in Honour of Gilles Kahn 2009), Computational Geometry (TPHOLs 2001), User Interfaces for Theorem Proving (JSC 1998, with L. Théry), Exact Real number computation and co-inductive types (Mathematical Structures in Computer Science 2007), mathematical computation and interactions with computer algebra (Mathematical Structures in Computer Science 2011, with A. Mahboubi and F. Guilhot, JAR 2017, with L. Rideau and L. Théry). He wrote an introductory book on the coq system that was published in 2004. He participated to a few landmark results of formally verified software and mathematical results, like Compcert (Types’04, with B. Grégoire and X. Leroy) and the machine-checked proof of the odd order theorem (ITP 2013, with G. Gonthier and team). Recent work has concentrated on proofs at the interface of analysis and algebra and their formal verification in Coq (CPP’16, formal proof of transcendence for e and pi as an application of Multivariate and Symmetric Polynomials, with S. Bernard, L. Théry, and P.-Y. Strub, JAR’17, Distant Decimals of PI, with L. Rideau and L. Théry). Current work is concerned with trajectory computation and formal proof of absence of collision.
Thierry Coquand (online lecture)
John Harrison
John Harrison is a Senior Principal Applied Scientist in the Automated Reasoning Group at Amazon Web Services, where he has among other things worked on a library of verified arithmetic for cryptographic applications. He received his PhD from the University of Cambridge in 1996 and has worked in both academia and industry on a variety of topics in automated theorem proving, formal verification and the design of numerical software. He is the primary developer of the HOL Light interactive theorem prover and author of the textbook “Handbook of Practical Logic and Automated Reasoning”.
Angeliki Koutsoukou-Argyraki
Angeliki Koutsoukou-Argyraki is a mathematician working at the
Computer Laboratory of the University of Cambridge.
Nikolai Kudasov
Nikolai Kudasov is a senior instructor and researcher at Innopolis University (Tatarstan, Russia) with a background in software engineering. Nikolai’s research interests lie with (functional) programming languages, type theory, and category theory. He is currently working on an experimental proof assistant rzk based on Riehl and Shulman’s type theory for synthetic ∞-categories introduced in 2017.
Jannis Limperg
Conor McBride
Leonardo de Moura (online lecture)
Paige Randall North
Emily Riehl
Emily Riehl is a Professor of Mathematics at Johns Hopkins University in Baltimore working in higher category theory and homotopy type theory. She has recently embarked on a collaborative project to formalize aspects of infinity-category theory in the computer proof assistant rzk. This proof assistant, developed by Nikolai Kudasov, is based on the simplicial type theory introduced in a joint paper with Mike Shulman, a formal system which has semantics in the category of simplicial objects in any infinity-topos.