Ce projet propose une bibliothèque Rocq (anciennement Coq) qui automatise la traduction d'une partie de la bibliothèque HOL-Light dédiée à la logique. L'objectif est de permettre une utilisation idiomatique des types et fonctions de HOL-Light dans Rocq, facilitant ainsi l'interopérabilité entre ces deux systèmes de preuve formelle. Les théorèmes traduits sont fournis sous forme d'axiomes pour optimiser les performances.