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: 23-25 January 2024

Remark: the official dates of the meeting taken into account for reimbursements are from January 23 to January 25 (3 days). However, since most people will arrive on January 22 and leave on January 26, the program includes two optional work sessions on January 22 afternoon and January 26 morning for the people who will be there.

Venue: Hotel Phoebus, Boulevard de Planasse 11430 Gruissan, France

How to get there? Hotel Phoebus is 26 minutes away by bus from Narbonne train station, and 2h10 by public transport from Montpellier airport MPL. There are many direct trains from Paris Gare de Lyon to Narbonne: 08:26-12:46, 09:42-14:24, 11:46-16:13, 14:56-19:20, 16:56-21:20, 17:42-22:20. If many people arrive at the same time, we may organize a private shuttle.

Program: Discussing the encoding in Dedukti of logical features (universe polymorphism with impredicativity, type classes, etc.), working alone or in small groups on the development of tools for generating, handling or transforming Dedukti files, taking advantage of the participation of experts on Dedukti or other languages and tools, working on the translation of proofs from one system to another system, to make progress on EuroProofNet objectives and deliverables.

Application procedure: The number of participants is limited. If you want to be funded, check the eligibility rules and send a mail to Frédéric Blanqui with the following information and documents:

  • URL of your homepage
  • planned date and time of arrival
  • planned date and time of departure
  • cost of travel in euros with quote (screen capture)
  • work plan: describe what you would like to do

Cost: Participants have to organize their travel by themselves. For accommodation and meals, they will have to pay to the hotel 30% in advance (that can be reimbursed in case of cancellation before January 14) and the remaining on site. See the reimbursement rules for more details. The daily allowance is fixed at 120 euros.

Participants (17):

  • Rishikesh Vaishnav will work on lean2dk.

  • Théo Winterhalter plans to work on extending Dedukti with decision procedures.

  • Thomas Traversié will work on the constructivisation of classical proofs.

  • Frédéric Blanqui will work on hol2dk, isabelle_dedukti and lambdapi.

  • Thiago Felicissimo will work on CompLF.

  • Abdelghani Alidra: hands-on learning of the encoding of logical features in Dedukti, discuss with other participants the current and the desired features and development workflow, meet and network with other EuroProofNet community members.

  • Gabriel Hondet will work on Lambdapi and STTfaxport.

  • Claude Stolze will work on the translation and verification of Atelier B proofs in Lambdapi, B-pog-translator.

  • Alessio Coltellacci with work on the encoding of Alethe proofs from SMT solvers to Lambdapi.

  • Nicolas Magaud will investigate how to use the Dedukti/Lambdapi toolchain to transform the Isabelle/HOL formal description of Faradžev-Read algorithm into an equivalent formal description in Coq.

  • François Thiré will work on Dedukti and STTfaxport.

  • Claudio Sacerdoti Coen plans to work on importing/exporting from Matita to Dedukti and developing a type checker for Dedukti written in Rust using term graphs.

  • Melanie Taprogge will work on the encoding of the THF proofs and the verification of LEO-III proofs in Dedukti/Lambdapi.

  • Bruno Barras plans to work on Lambdapi (reduction engine, use of de Bruijn indices).

  • Filip Maric will work on using Dedukti/Lambdapi (esp. isabelle_dedukti) to translate a whole Isabelle/HOL development into a similar one in Coq.

  • David Delahaye will work on extending the Dedukti/Lambdapi outputs of ZenonModulo to handle arithmetic proofs.

  • Isaac Lluis will work on extending the Dedukti/Lambdapi outputs of ZenonModulo to handle arithmetic proofs.

Monday 22 January (optional, for people arriving the day before the meeting):

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)

Tuesday 23 January:

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 24 January:

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 25 January:

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 26 January (optional, for people leaving after the meeting):

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