July 31-August 4, 2023
Fourteenth Conference on Interactive Theorem Proving
Białystok, Poland, 2023
ITP 2023 Organization
Program co-chairs
Adam Naumowicz (University of Bialystok)
René Thiemann (University of Innsbruck)
Program Committee
| Andreas Abel | Gothenburg University |
| Jesús Aransay | Universidad de La Rioja |
| Jeremy Avigad | Carnegie Mellon University |
| Mauricio Ayala-Rincon | Universidade de Brasília |
| Christoph Benzmüller | University of Bamberg |
| Jasmin Blanchette | Vrije Universiteit Amsterdam |
| Sandrine Blazy | University of Rennes 1 – IRISA |
| Sylvie Boldo | Inria and Université Paris-Saclay |
| Cyril Cohen | Université Côte d'Azur - Inria |
| Liron Cohen | Ben-Gurion University |
| Luis Cruz-Filipe | University of Southern Denmark |
| Ruben Gamboa | University of Wyoming |
| Jason Gross | Massachusetts Institute of Technology |
| John Harrison | Amazon Web Services |
| Hugo Herbelin | INRIA |
| Cezary Kaliszyk | University of Innsbruck |
| Chantal Keller | Université Paris-Saclay |
| Peter Lammich | University of Twente |
| Andreas Lochbihler | Digital Asset GmbH |
| Marco Maggesi | Università degli Studi Firenze |
| Assia Mahboubi | INRIA |
| Magnus O. Myreen | Chalmers University of Technology |
| Cláudia Nalon | University of Brasília |
| Adam Naumowicz (co-chair) | University of Bialystok |
| Tobias Nipkow | Technical University of Munich |
| Michael Norrish | Australian National University |
| John O’Leary | Intel |
| Lawrence Paulson | University of Cambridge |
| Andrei Popescu | University of Sheffield |
| Bas Spitters | Aarhus University |
| René Thiemann (co-chair) | University of Innsbruck |
| Josef Urban | Czech Technical University in Prague |
| Makarius Wenzel | sketis.net |
| Freek Wiedijk | Radboud University Nijmegen |
| Akihisa Yamada | National Institute of Advanced Industrial Science and Technology |
Local organizers
Mizar group at the University of Bialystok (UwB) and Polish Information Processing Society (PTI) - Sekcja Analizy Danych- Artur Kornilowicz (UwB, PTI)
- Adam Grabowski (UwB, PTI)
- Karol Pak (UwB)
- Czeslaw Bylinski (UwB)
- Roman Matuszewski (UwB)
Extra motivation for organizing the meeting in 2023 - 50 years of the Mizar project
From R. Matuszewski and P. Rudnicki - MIZAR: the first 30 years:
(...) The first presentation of the MIZAR ideology understood here as visionary speculation was presented by Andrzej [Trybulec] on November 14, 1973 at a seminar in the Institute of Library Science and Scientific Information at Warsaw University. During the seminar Andrzej postulated a language for recording mathematical papers such that:
- the papers could be stored in a computer and later, at least partially, translated into natural languages,
- the papers would be formal and concise,
- it would form a basis for the construction of an automated information system for mathematics,
- it would facilitate detection of errors, verification of references, elimination of repeated theorems, etc.
- it would open a way to machine assisted education of the art of proving theorems,
- it would enable automated generation of input into typesetting systems.
Contact
If you have any problems or questions, please contact us via e-mail at: itp2023@mizar.uwb.edu.pl