Ce projet propose une bibliothèque Rocq (anciennement Coq) qui traduit automatiquement la bibliothèque HOL-Light dédiée à la logique. Il permet de manipuler des types et fonctions idiomatiques en Rocq tout en conservant les propriétés et théorèmes originaux. L'objectif est de faciliter l'interopérabilité entre ces deux environnements de preuve formelle pour des applications en vérification mathématique et en intelligence artificielle.