EuroProofNet Workshop on the development, maintenance, refactoring and search of large libraries of proofs

This meeting is part of the Computational Logic Autumn Summit 2022.

Date: 23-24 September 2022

Venue: Tbilisi State University, Chavchavadze ave. 1, 0179 Tbilisi, Georgia, room 202

Registration: Registration is free but mandatory. To attend the workshop, physically or online, please send a mail to Frédéric Blanqui. Connection instructions will be sent to online participants a few days before the event.

If you are interested in giving a talk, please send a mail to Frédéric Blanqui with a title and abstract. We welcome talks, tutorials, demos, on library descriptions or on methodologies, algorithms and tools trying to tackle the challenges raised by the development, maintenance, refactoring and search of large libraries of proofs. We especially welcome talks on search tools.

Programme: here

Talks:

Claudio Sacerdoti (University of Bologna), The challenges of the EuroProofNet Working Group 4 on libraries (slides)
Fabian Huch (Technical University of Münich) and Yiannis Stathopoulos (University of Cambridge), Finding facts in large formalization libraries: two Isabelle/AFP attempts (slides)
Anne Baanen (Vrije Universiteit Amsterdam), Bundling in Dependent Type Theory (slides)
Riccardo Brasca (University of Paris Cité), Maintenance of Lean’s mathlib and the Liquid tensor experiment (slides)
Florian Rabe (University of Erlangen), Experiences from Exporting Major Proof Assistant Libraries (slides)
Alexander Best (Vrije Universiteit Amsterdam), Metaprogramming for Automation of Library Maintenance (slides)
Reuben Rowe (Royal Halloway University of London), Refactoring OCaml (slides)
Georges Gonthier (INRIA Saclay), First-class object hierarchies [online] (slides)
Enrico Tassi (INRIA Sophia Antipolis), Hierarchy Builder, algebraic hierarchies made easy (in Coq) [online] (slides)
Geoff Sutcliffe (University of Miami), Proofs and Models in the TPTP World [online] (slides)
Artur Korniłowicz (University of Bialystok), XML-based representation of Mizar Mathematical Library [online] (slides)
André Freitas (University of Manchester), Natural Language & Proofs: A Neuro-symbolic Perspective (slides)
Marco Maggesi, The HOL Light library of formalized mathematics (slides)
Roland Coghetto and Julien Narboux (University of Strasbourg) [online], The GeoCoq library and its porting to Isabelle (slides)
Talia Ringer (University of Illinois at Urbana-Champaign) [online], Concrete Problems in Proof Automation (slides) (AITP video)

On site participants (24): Frédéric Blanqui, Claudio Sacerdoti, Fabian Huch, Yiannis Stathopoulos, Anne Baanen, Riccardo Brasca, Alexander Best, Reuben Rowe, Marco Maggesi, André Freitas, Maribel Fernandez, Carsten Fuhs, Peter Ölveczky, Sandra Alves, Volker Stolz, Besik Dundua, Luigi Liquori, Alicia Villanueva, Ashvni Narayanan, Ramon Fernández Mir, Santiago Escobar, Peter Koepke, Erika Abraham, Temur Kutsia

Online participants (65): Georges Gonthier, Enrico Tassi, Geoff Sutcliffe, Artur Korniłowicz, Roland Coghetto, Julien Narboux, Florian Rabe, Talia Ringer, Christian Sottile, Georgios Pitsiladis, Dara MacConville, Adam Naumowicz, Stepan Holub, Boris Djalal, Stefania Dumbrava, Tjark Weber, Andreas Nuyts, Jørgen Villadsen, Rafael Castro Goncalves Silva, Muharrem Tuncay Gençoğlu‬, Angeliki Koutsoukou Argyraki, Yosuke Ito, Gidon Ernst, Cesare Tinelli, Michail Karatarakis, Bart Michels, Cezary Kaliszyk, Anthony Bordg, Carlos Olarte, Parivash Feyzishendi, Emilio Jesús Gallego Arias, Assia Mahboubi, Ana Borges, Guillaume Allais, Mitsuharu Yamamoto, Reynald Affeldt, Brendan Mahony, Dmitriy Traytel, Wolfgang Windsteiger, Florian Sextl, Alexander Rademaker, Paqui Lucio, Paul Jackson, Adrian Riesco Rodriguez, Stephan Schulz, Wenda Li, Pierre-Yves Schobbens, Nicolas Magaud, David Cerna, Amélie Ledein, Emilie Grienenberger, Darren Rhea, Sergei Soloviev, Roman Matuszewski, Sushma Akoju, Christoph Schwarzweller, Jason Rute, Daniel Ventura, Mariano Moscato, Filippo A. E. Nuccio Mortarino Majno di Capriglio, Andrei Klimov, Bruno Xavier, Tanner Slagel, Peeyush Kushwaha, Cyril Cohen

Scientific organizers: Frédéric Blanqui and Claudio Sacerdoti

Local organizer: Besik Dundua

Funding application deadline passed. EuroProofNet can reimburse the transport to Tbilisi + 60 euros/day for the accommodation on September 23-24 for a number of participants. Please check eligibility rules and reimbursement rules to get more details.

Computational Logic Autumn Summit 2022: This meeting is part of the Computational Logic Autumn Summit 2022 which includes: