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.

Organizer: Frédéric Blanqui

Date: 25-28 July 2023

Venue: La Résidence, 5 rue des Mousses, 88340 Le Val d’Ajol, France

How to get there? There are direct trains from Paris to Remiremont train station (East of France). A shuttle will be organized from Remiremont train station and the hotel on July 24 at 15:15, and from the hotel to Remiremont train station on July 28 at 15:15. Le Val d’Ajol is also 1h30 away by car from Bâle airport, and 3h by car from Luxembourg, Karlsruhe or Zurich. There are also a few buses between Remiremont and Val d’Ajol.

Programme: Working individually or in small groups on the development of tools to make progress on the deliverables consisting of databases or software developments.

Cost: The cost of accommodation and meals is 150 euros/day/person. EuroProofNet can reimburse to a limited number of people the transport + a daily allowance for the accommodation and meals for a number of participants with the following priorities: contribution to EuroProofNet objectives and deliverables, people from COST inclusiveness target countries, young researchers, under-represented genders. Check eligibility rules and reimbursement rules to get more details.

Registration and funding application: Deadline: 14 May 2023. The number of participants is limited. If you want to participate, apply to EuroProofNet if not already done, and fill in the following application form. Applicants will be notified by May 18. Accepted participants will then have to make a bank transfer of half of the cost to La Résidence (IBAN: FR7617206002135619393901050) in order to confirm their participation. In case of cancellation before July 21, they will be reimbursed. The second half will have to paid at the hotel.

Participants:

  • Frédéric Blanqui fixed ZenonModulo to generate proofs where the negated conjecture is taken as hypothesis instead of as axiom, and improved the translation hol2dk from HOL-Light to Coq. He also helped Claudio Sacerdoti and Geoff Sutcliffe with Lambdapi, and Geoff Sutcliffe with ZenonModulo.

  • Jesper Cockx worked on refactoring a library for well-scoped syntax representations in Agda (code). This is intended to be used in the Agda Core project to specify the typing rules of a core language for Agda in Agda, which will improve interoperability between Agda and other languages.

  • Simon Guilloud and Amélie Ledein have continued a reduction of the Sequent Calculus system to Natural Deduction and lambda calculus (using Curry-Howard) inside Lambdapi thanks to rewriting rules. This work has started during the Dedukti meeting in January. They have also presented their work around LISA and K respectively.

  • Gilles Dowek presented his work on deskolemization (slides, paper) and has discussed with several members of the meeting about the implementation of a deskolemization algorithm.

  • Rishikesh Vaishnav worked on his Lean2Dk implementation for translating Lean into Dedukti, and made progress on the Pure Type System -> lambda-Pi-calculus modulo embedding.

  • Claudio Sacerdoti worked on implementing a search engine for LambdaPI. He completed the implementation started during the meeting in January and he added a web interface.

  • Alessio Coltellacci worked on the reconstruction of Alethe SMT proof format in Lambdapi. He is adding a new module for exporting Lambdapi proof in the SMT proof checker Carcara. He started to add the rational number to the standard library of Lambdapi so we will be able to integrate Zenon-modulo-generated proof in the current goal when the tactic why3 is run.

  • Pascal Fontaine worked on several libraries for a modular approach to SMT reasoning. After the seminar, an SMT3 parser started working, and a library to represent and handle SMT3 terms has been designed and was to some extent usable. This project is related to EuroProofNet in the sense that this set of libraries can be used to create proof producing tools (all libraries will be themselves proof producing with detailed proofs), and can also be useful for tools handling proofs from automated solvers.

  • Stephan Schulz improved the TPTP proof output of the ATP PyRes to match inout expected by several TPTP processing tools. He also modified the prover E to provide additional explicit type information in TFF/THF proofs, that, while not required by the TPTP standard, is expected by some tools, and performed further work on E.

  • Geoff Sutcliffe
    1. Worked with Stephan Schulz to upgrade the proof output from his PyRes prover so that it is TPTP-compliant, so that the proofs can be viewed in the IDV derivation viewer in SystemOnTSTP (part of the TPTP World). That work was instigated by Claudia Schon from the University of Koblenz-Landau, who uses PyRes and IDV in her research.
    2. Worked with Frédéric Blanqui with the aim of completing the embedding of LambdaPi output from the GDV proof verifier (part of the TPTP World). We were so close when I had to leave, and I believe it will be done this week. This also motivated further work to provide remote access to the SystemOnTPTP server (part of the TPTP World) in Miami so that ZenonModulo can be accessed remotely from GDV. That will make it unnecessary to have SystemOnTPTP installed locally. Frederic has added information about the extended GDV tool to the COST action web site.
    3. Discussed the issue of verifying Skolemization steps with various attendees, and learned how Dedukti deals with it from Gilles Dowek’s presentation. He presented the algorithm implemented in the SKonverto tool, which might be useful in GDV for generating LambdaPi output for Skolemization steps.
    4. Explained what I have been doing to Jesper Cockx, who leads WG1 of the COST action. I joined WG1 and provided the relevant papers to Dmitry Traytel to be added to the COST action web site.

  • David Delahaye has tested the latest version of Zenon Modulo (development version) on the BWare project benchmark. The results showed (with a low timeout of 3s) that we obtained similar results (10,459 proofs obtained over 12,828 problems) to the version of Zenon Modulo used in the BWare project (in 2016). David Delahaye also worked on the Lambdapi output for the Goéland automated deduction tool (based on tableaux and the use of concurrency).

  • Isaac Lluís worked with David Delahaye and Olivier Hermant to test ZenonModulo on a few thousand problems to see if it needed updating. He also worked on the LambdaPi output for the concurrent theorem prover Goéland, taking advantage of the presence of the Deducteam.

  • Olivier Hermant worked on the lambdapi output of the automated theorem provers Zenon Modulo and Goéland, and on the implementation of an algorithm to change numeric base, on which he gave a short presentation.

  • Wojciech Loboda worked on the definition and the implementation of an algorithm to change numeric base, after an article of Jean-Paul Delahaye published in Pour la Science No 519

Monday 24 July: (for those arriving on July 24)

15:15-15:45 shuttle
15:45-16:00 check-in
16:00-16:15 coffee break
16:15-18:15 work session 1
18:15-19:30 free time
19:30-21:00 dinner
21:00-23:00 work session 2 (optional)

Tuesday 25 July:

08:00-08:30 breakfast
08:30-10:30 work session 1
10:30-10:45 coffee break
10:45-12:45 work session 2
12:45-14:00 lunch
14:00-16:00 work session 3
16:00-16:15 coffee break
16:15-18:15 work session 4
18:15-19:30 free time
19:30-21:00 dinner
21:00-23:00 work session 5 (optional)

Wednesday 26 July:

08:00-08:30 breakfast
08:30-10:30 work session 1
10:30-10:45 coffee break
10:45-12:45 work session 2
12:45-14:00 lunch
14:00-16:00 work session 3
16:00-16:15 coffee break
16:15-18:15 work session 4
18:15-19:30 free time
19:30-21:00 dinner
21:00-23:00 work session 5 (optional)

Thursday 27 July:

08:00-08:30 breakfast
08:30-10:30 work session 1
10:30-10:45 coffee break
10:45-12:45 work session 2
12:45-14:00 lunch
14:00-16:00 work session 3
16:00-16:15 coffee break
16:15-18:15 work session 4
18:15-19:30 free time
19:30-21:00 dinner
21:00-23:00 work session 5 (optional)

Friday 28 July:

08:00-08:30 breakfast
08:30-10:30 work session 1
10:30-10:45 check out & coffee break
10:45-12:45 work session 2
12:45-14:00 lunch
14:00-15:00 free time
15:00-15:45 shuttle