• France:
  • Frédéric Blanqui (French PI)
  • Théo Winterhalter
  • Anthony Bordg
  • Catherine Dubois
  • Yoan Géran (PhD student)
  • Rishikesh Vaishnav (PhD student)
• Japan:
  • Reynald Affeldt
  • Akihisa Yamada
  • Jérémy Dubut

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 April 2024: Translating HOL-Light proofs to Coq, 18 pages, accepted at LPAR
• 5 March 2024: Sharing proofs with predicative theories through universe polymorphic elaboration, Frédéric Blanqui and Thiago Felicissimo, 38 pages, accepted for publication in LMCS
• 26 February 2024: new releases of lambdapi, hol2dk and coq-hol-light
• 21 February 2024: Translating HOL-Light proofs to Coq, 18 pages, submitted

Visits:

• 21 October - 1st November 2024: visit of AIST by Frédéric Blanqui
• 7-17 May 2024: visit of AIST by Théo Winderhalter

Software developed:

• isabelle_dedukti: Isabelle to Dedukti translator
• lambdapi: Dedukti to Coq translator
• coqine: Coq to Dedukti translator

Related work and tools:

• Hol2dk: HOL-Light to Dedukti and Coq translator
• HOL Import: translator from HOL-Light to Isabelle [old version] [new version]