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:

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 and Claudio Sacerdoti

Local organizer: Besik Dundua

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