European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

Date: 13-14 September 2024

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

This meeting includes several sessions shared with other co-located events. Registration to these other events is mandatory (see the ITP web page for this).

September 13:

  • 15th Conference on Interactive Theorem Proving (ITP’24)

    time title, authors
    09:00 Invited talk: Translating libraries of definitions and theorems between proof systems, Frédéric Blanqui
    10:00 Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4, Sam Ezeh
    10:15 Formalising Half of a Graduate Textbook on Number Theory, Manuel Eberl, Anthony Bordg, Lawrence Paulson and Wenda Li
    10:30 break
    11:00 An Isabelle/HOL formalization of narrowing and multiset narrowing for E-unifiability, reachability and infeasibility, Dohan Kim
    11:30 A Modular Formalization of Superposition in Isabelle/HOL, Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette and Sophie Tourret
    12:00 A Proof-Producing Superposition Theorem Prover for Dependent Type Theory, Joshua Clune, Yicheng Qian, Alexander Bentkamp and Jeremy Avigad
    12:30 lunch
    14:00 Mechanized HOL Reasoning in Set Theory, Simon Guilloud, Sankalp Gambhir, Andrea Gilot and Viktor Kuncak
    14:30 End-to-End Formal Verification of a Fast and Accurate Floating-Point Approximation, Florian Faissole, Paul Geneau de Lamarlière and Guillaume Melquiond
    15:00 Distributed Parallel Build for the Isabelle Archive of Formal Proofs, Fabian Huch and Makarius Wenzel
    15:30 break

  • 2nd Workshop on the development, maintenance, refactoring and search of large libraries of proofs

    time title, authors
    16:00 Exploring the benefits of a general abstract formalization, Thaynara Arielly de Lima
    16:30 Post-processing Coq Proof Scripts to Make Them More Robust, Titouan Lozac’h and Nicolas Magaud
    17:00 Verifying Nominal Equational Reasoning Modulo Algorithms, Mauricio Ayala-Rincón
    17:30 An Indexer and Query Language for Libraries written in LambdaPi/Dedukti, Claudio Sacerdoti Coen

September 14:

time title, authors
9:40 On the Potential of Coq as the Platform of Choice for Hardware Design, Sebastian Ertel, Max Kurze and Michael Raitza
10:00 A Development Process for Coq Projects Permitting Invalid Proofs, Hendrik Tews
10:30 break
11:00 CoqPilot, a plugin for LLM-based generation of proofs, Andrei Kozyrev, Gleb Solovev, Nikita Khramov and Anton Podkopaev
11:30 Blueprints for formalisation in Coq, Peter Lefanu Lumsdaine
11:50 Coq Platform docs: A Compilation of Short Interactive Tutorials and How-To Guides for Coq, Thomas Lamiaux, Pierre Rousselin and Théo Zimmermann
12:20 lunch
14:00 Shared invited talk: From 100 to 1000+ theorems, Freek Wiedijk
15:00 Lessons from Formalizing (Higher) Category Theory, Benedikt Ahrens and Niels van der Weide
15:30 break
16:00 Towards Formalising the Guard Condition of Coq, Yee Jian Tan and Yannick Forster
16:25 Turning the Coq Proof Assistant into a Pocket Calculator, Guillaume Melquiond
16:45 Discussion with Coq developers
18:00 end
time title, authors
09:20 Welcome by Tobias Nipkow
09:30 A formalized programming language with speculative execution, Jamie Wright and Andrei Popescu
10:00 A programming language for controlling robots (work in progress), Artur Graczyk, Marialena Hadjikosti and Andrei Popescu
10:30 break
11:00 Isabelle proof terms revisited, Makarius Wenzel
11:30 Isabelle as Systems Platform: Managing Automated and Quasi-interactive Builds, Fabian Huch
12:00 Isabelle/DOF: Extended Abstract and Tool Demonstration, Achim D. Brucker, Idir Ait-Sadoune, Nicolas Méric and Burkhart Wolff
12:30 lunch
14:00 Shared invited talk: From 100 to 1000+ theorems, Freek Wiedijk
15:00 HOL Light to Isabelle/HOL Translation, Rebooted, Ghilain Bergeron, Stéphane Glondu and Sophie Tourret
15:30 break
16:00 Verified Preprocessing of Linear Integer Arithmetic Constraints, René Thiemann
16:30 Time-Aware Stream Processing in Isabelle/HOL, Rafael Castro Gonçalves Silva and Dmitriy Traytel
17:00 A Formalization of Sequent Calculus for Classical Implicational Logic, Frederik Krogsdal Jacobsen and Jørgen Villadsen
17:30 Project Proposal: Reinforcement learning on the Isabelle proof assistant, Jonathan Julian Huerta Y Munive

Call for talk proposals: If you are interested in giving a talk at the 2nd Workshop on the development, maintenance, refactoring and search of large libraries of proofs, send a mail to Frédéric Blanqui with a title and short 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.

Registration: Registration to the 2nd Workshop on the development, maintenance, refactoring and search of large libraries of proofs is free but mandatory. To attend the workshop, please send a mail to Frédéric Blanqui.

Funding application: If you are attending the Isabelle workshop, the Coq workshop, the ITP conference or the 2nd Workshop on the development, maintenance, refactoring and search of large libraries of proofs, and want to be reimbursed of your transport to Tbilisi, and of your accommodation and meals between September 12 and September 15, following the COST reimbursement rules, with a daily allowance of 80 euros, you need to:

  • check your eligibility
  • register to at least one EuroProofNet working group
  • send a mail to Frédéric Blanqui with the following information: departure date from home, return date at home, and estimation in EUROS of the transport to Tbilisi with a screen capture

Funded participants (13): Abdelghani Alidra, Claudio Sacerdoti Coen, Clement Pit-Claudel, Ján Perháč, Luca Pasetto, Mauricio Ayala-Rincon, Max Zeuner, Muhammad Usama Sardar, Natalia Slusarz, Nicolas Magaud, Simon Guilloud, Thaynara Arielly de Lima, Théo Winterhalter

Scientific organizers: Frédéric Blanqui, Angeliki Koutsoukou Argyraki, Claudio Sacerdoti for the workshop on libraries, Yves Bertot for ITP, Théo Winterhalter and Clément Pit-Claudel for the Coq workshop, Makarius Wenzel for the Isabelle workshop

Local organizer: Besik Dundua

Previous workshop: 1st EuroProofNet Workshop on the development, maintenance, refactoring and search of large libraries of proofs