Interoperability of Rocq and Isabelle proof systems


Participants:

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.

News:

Online meetings:

Visits:

Publications:

Software:

Related work and tools:


Statcounter W3C Validator Last updated on 1 September 2025. Come back to main page.