Posted by Jesper on October 15, 2021
EuroProofNet is the European research network on digital proofs. It aims at boosting the interoperability and usability of proof systems. It gathers 190 researchers on proof systems and formal proofs, from 30 different countries.
Together with Catherine Dubois, I am leading the working group on Tools for Proof Systems Interoperability. In particular, we will coordinate developers of various proof systems (dependently typed ones like Coq and Agda, but also others such as Isabelle/HOL, Event-B, and TLA+) who want to translate proofs between these systems using the Dedukti logical framework as an intermediate language.
You can find more information about this and the other working groups on our website (still work-in-progress at the moment of writing). If you are interested to work on this, please consider applying to join the working group and/or get in touch!