Scientific objective:
This collaboration aims at making the two main proof assistants
currently used in the world, Isabelle and Rocq, interoperable, by first
translating Isabelle and Rocq libraries to Dedukti, and then the
obtained Dedukti libraries to Isabelle and Rocq, possibly after some
transformations.
22 July - 2 august 2024: Frédéric Blanqui and Rishikesh Vaishnav gave presentations of hol2dk and lean2dk at the Hausdorff trimester program on "prospects of formal mathematics", and discuss about the translation of Isabelle type classes to Rocq with Makarius Wenzel and Mario Carneiro, and about trocq with Assia Mahboubi
27 November 2024: discussion on ongoing and planned activities
9 July 2024: presentation of Isabelle type classes by Akihisa, presentation of Rocq type classes by Théo, presentation of Hierarchy Builder by Reynald
17 June 2024: presentation of isabelle_dedukti by Akihisa, presentation of hol2dk by Frédéric
Visits:
8-17 December 2025: visit of AIST by Frédéric Blanqui and Antoine Gontard
16-20 December 2024: visit of AIST by Ciarán Dunne and Melanie Taprogge
Ciarán and Melanie worked with Akihisa Yamada and Reynald Affeldt. They presented their ongoing work on translating proofs from automated theorem provers to Lambdapi (cvc5 and Leo-III respectively).
Akihisa presented his Isabelle formalization of abstract structures like groups and rings as locales. He demonstrated how these locales could be extended to provide a generic interface for the natural numbers. He explained that the eventual goal of this work was to share theorems between the representation of the natural numbers imported from Rocq and the native natural numbers of Isabelle.
Using knowledge obtained during his PhD project, Ciarán helped solve some problems with Akihisa's usage of Isabelle's Lifting and Transfer packages; namely providing formal proofs for the 'transfer rules' on quantifiers, and giving guidance on automating the transformation of terms using these rules.
Akihisa also presented a particular namespace problem encountered when translating formalizations from Isabelle to Dedukti. Furthermore, they discussed the current implementation of the tool isabelle_dedukti and the future maintenance thereof, in which Melanie is going to assist. Towards this, Melanie began learning the basics of the Isabelle build system, mainly relating to the structure of the session and theory hierarchies.
21 October - 1st November 2024: visit of AIST by Frédéric Blanqui
Comparison of the definitions of number types (natural numbers, integers, rationals and reals) in HOL-Light, Isabelle and Rocq.
