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

Chairs: Frederic Blanqui and Claudio Sacerdoti Coen

23-24 September 2022

Proof libraries are becoming bigger and bigger. They can contain tens of thousands of files and hundreds of thousands of objects (type, definition, theorem). Their development, maintenance, refactoring and search raises challenging problems. This workshop aims at gathering researchers working on these problems to present libraries or methodologies, algorithms and tools trying to tackle these problems.

This workshop is proposed by the COST action 20111 EuroProofNet. EuroProofNet is the European research network on digital proofs. It aims at boosting the interoperability and usability of proof systems. It is a COST action started on November 2021 now gathering more than 270 researchers from 42 different countries, organized in 6 working groups: interoperability, automated theorem provers, program verification, proof libraries, machine learning, and type theory. The WG4 on proof libraries wants to investigate various approaches to efficiently maintain libraries of formal proofs. The goal is to make a collection of proofs that can be modified, extended, and queried by users who do not have expert knowledge of the entire collection nor of the system that was used to develop the proofs.

The workshop will be hybrid. It will consist of talks, tutorials or demos, and will have a discussion session as well. The organizers will directly contact potential speakers, and send some open call for contributions if needed. There will be no proceedings but abstracts, slides and videos will be posted on the EuroProofNet web site. EuroProofNet will reimburse the transport to Tbilisi and the accommodation on September 23-24 of a number of participants.