• France:
  • Frédéric Blanqui (French PI)
  • Théo Winterhalter
  • Catherine Dubois
  • Rishikesh Vaishnav (PhD student)
  • Melanie Taprogge (PhD student)
  • Ciarán Dunne (postdoc)
  • 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:

• 4 November 2024: release of a Coq library of 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:

• 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:

• 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]