Dedukti tools developers meeting 2
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 coded a prototype implementation of CompLF (Computational Logical Framework, name subject to change), a logical framework in the tradition of Dedukti whose full definition and metatheoretical study is still a work in progress. Like Dedukti, CompLF is a framework for defining type theories whose definitional equality is purely computational, in the sense that it is purely generated by rewrite rules. It refines Dedukti by incorporating canonical forms (as in Canonical LF) and erased arguments, allowing for a strong syntactic correspondence with commonly used non-annotated syntaxes. Because erasing arguments from the syntax can jeopardize decidability of typechecking, CompLF theories can be polarized by assigning modes to their symbols and their non-erased arguments. Terms written in these polarized theories can then be typechecked through a (theory agnostic) bidirectional typing algorithm. This algorithm is the one implemented in the prototype, which has been successfully tested with a small test suite. The next steps are to further test the implementation and conclude the metatheoretical study of CompLF.
-
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.
-
Julien Narboux and Predrag Janičić 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.
-
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.
-
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. They 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. They also have 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 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) |
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 arriving 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 |
