• France:
  • Frédéric Blanqui (French PI)
  • Théo Winterhalter
  • Catherine Dubois
  • Rishikesh Vaishnav (PhD student)
  • Melanie Taprogge (PhD student)
  • Ciarán Dunne (postdoc)
  • Bruno Barras
  • Jérémy Dubut (initially in Japan, now at LIX)
• Japan:
  • Reynald Affeldt
  • Akihisa Yamada

Scientific objective: This collaboration aims at making the two main proof assistants currently used in the world, Isabelle and Coq, interoperable, by first translating Isabelle and Coq libraries to Dedukti, and then the obtained Dedukti libraries to Isabelle and Coq, possibly after some transformations.

News:

• 17 December 2024: complete translation of HOL-Light base library in Coq
• 4 November 2024: release of a Coq library of the definition of reals in HOL-Light
• 13 September 2024: Translating libraries of definitions and theorems between proof systems (invited talk), 15th International Conference on Interactive Theorem Proving, (ITP'24) , Tbilisi, Georgia
• 4 April 2024: Translating HOL-Light proofs to Coq, 18 pages, accepted at LPAR
• 26 February 2024: new releases of lambdapi, hol2dk and coq-hol-light

Online meetings:

• 27 November 2024: discussion on ongoing and planned activities
• 9 July 2024: presentation of Isabelle type classes by Akihisa, presentation of Coq 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:

• 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 Coq 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 Coq.
  • Exploration of Cyril Cohen's Coq library on quotients.
  • Reproduction of Isabelle definitions of number types in Coq.
  • Reproduction of Coq definitions of number types in Isabelle.
  • In isabelle_dedukti, transformation of equational axioms defining type classes into definitions.
  • Exploration of the use of Coq type classes and Coq plugin Hierarchy Builder for reproducing Isabelle type classes in Coq.
  • Adaptation of isabelle_dedukti to Isabelle2024.
  • Extension of hol2dk with the alignment of data types used to define real numbers in HOL-Light.
  • Extract a Coq library with the definition of real numbers in HOL-Light and publish it on opam.
• 7-17 May 2024: visit of AIST by Théo Winderhalter.
  • Start working on the alignment of the Coq and Isabelle libraries on measure theory [coq]

Publications:

• Translating HOL-Light proofs to Coq, Frédéric Blanqui, LPAR'24

Software:

• isabelle_dedukti: Isabelle to Dedukti and Lambdapi translator
• lambdapi: Dedukti and Lambdapi to Coq translator
• coqine: Coq to Dedukti translator
• hol2dk: HOL-Light to Dedukti, Lambdapi and Coq translator

Related work and tools:

• HOL Import: translator from HOL-Light to Isabelle [old version] [new version]