Organizer: Frédéric Blanqui

Date: 27-29 January 2023

Remark: the official dates of the meeting taken into account for reimbursements are from January 27 to January 29. However, since many people will arrive on January 26 and leave on January 30, the program includes two optional work sessions on January 26 afternoon and January 30 morning for the people who will be there.

Venue: Villa Clythia, 2754 avenue Henri-Giraud 83600 Fréjus, France

How to get there? Villa Clythia is at 3 km from the TGV train station of Saint Raphaël - Valescure, and 60 km from the Nice airport.

Programme: 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, to make progress on EuroProofNet objectives and deliverables. See previous meeting.

Application procedure: The number of participants is limited. If you want to participate, 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 to make progress on EuroProofNet objectives and deliverables

Cost: Participants will have to pay for their travel, bedroom and meals at Villa Clythia. To cover the bedroom and meals, the daily allowance is fixed at 110 euros. See the reimbursement rules for more details.

Participants (15):

  • Frédéric Blanqui fixed small bugs and made improvements in Lambdapi (943, 944, 949, 950, 952, 953, 954) and developed a new translator from HOL-Light to Dedukti and Lambdapi based on a fork of HOL-Light: see dk branch.

  • Thiago Felicissimo: Agda2Dedukti, Canonical Dedukti

  • Yoan Géran worked on a tool to translate proofs from a Dedukti encoding of the Predicate logic to the tactic language of Coq. He used it to translate the proofs of the first book of Euclid (from the Geocoq library) to Coq. The result is more readable than the one obtained previously using the export from STTFA.

  • Predrag Janičić: coherent logic and Larus to Dedukti

  • Julien Narboux and Predrag Janicic developed with the help of Artur Korniłowicz support for exporting proofs from their coherent logic prover called Larus to the proof assistant Mizar. Julien Narboux and Yohan Geran discussed the transformation of proofs into coherent logic form, the generation of tactic based proofs from predicate logic and the integration of the GeoCoq library into Logipedia.

  • Emilie Grienenberger: HOLLightToDk

  • Claudio Sacerdoti Coen and Enrico Tassi patched CoqInE to export type-class related information to Dedukti file (i.e. what symbols are typeclass declaration/instantces); wrote bash scripts to translate the CoqInE output to Lambdapi; embedded Elpi into Lambdapi (see PR#418) and used it to automatically find instances of type-classes, both natively and up to the encoding used in CoqInE. They also documented how to export Isabelle files not in the standard library to Lambdapi, with the aim of enriching the output with type class related annotations.

  • Amélie Ledein K and Metamath to Dedukti

  • Thomas Traversié worked on the elimination of the user-defined rewriting rules in a Dedukti theory. Such a transformation is done by replacing these rewriting rules with axioms. The main difficulty is to handle the different possible translations of a term, depending on where the rewriting rules are applied. He started to implement this technique.

  • Simon Guilloud and Amélie Ledein have implemented Sequent Calculus inside Lambdapi. Simon have explored variants of FOL where conjunctions and disjunctions are represented as lists and the possibility of using Lambdapi’s rewrite system to compute partial normal forms of formulas. He also has started a reduction of the Sequent Calculus system to Natural Deduction and lambda calculus (using Curry-Howard).

  • Claude Stolze finished implementing a translator from Atelier B proof obligations (in POG format) to Lambdapi. 5387 POG files (5.7 GiB) have been processed and the resulting Lambdapi files have been typechecked successfully. This will be the basis for proving these proof obligations using external tools.

  • Artur Korniłowicz worked on a tool for the fully automatic translation of definitions and statements (theorems, schemas, registrations, and reductions) collected in the Mizar Mathematical Library into Lambdapi. The first result is the translation of definitions and statements involving notions without hidden arguments. He also cooperated on the export of Larus proofs into the Mizar proof assistant.

  • Gabriel Hondet documented the exporter personoj (PVS to Dedukti) planning for a new release. He provided a quickstart guide, how-to guides to run the test suites and to check the output of personoj, and additional notes for developers of personoj. He also contributed to STTfaXport and released an initial beta version. He also documented a feature of Lambdapi (https://github.com/Deducteam/lambdapi/commit/7f1da661a9899f1d4f7a98ecf1619fc612eaa042) and discussed a revised API for Dedukti with François Thiré.

  • François Thiré worked on dkcheck, dkmeta, and universo, to make them robust and easier to interact with (in particular to get a modular proof exporter of the Isabelle proofs encoded into the STTfa logic). The main task was to provide users with an API that is safe and convenient. This work led to a new API which is better (especially regarding safety) and with less side-effects. This should help the future developments of interoperability projects using the Dk tools API. In particular, this should ease the integration with STTfaxport, a tool to export proofs from the logic STTfa to various proof systems.

Thursday 26 January (optional, for people who arrives 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)

Friday 27 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)

Saturday 28 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)

Sunday 29 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)

Monday 30 January (optional, for people who leaves 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