Ce projet propose une bibliothèque Rocq (anciennement Coq) qui automatise la traduction d'une partie de la bibliothèque HOL-Light en utilisant des outils dédiés. Il permet de mapper des types et fonctions de HOL-Light vers des constructions idiomatiques dans Rocq, facilitant ainsi l'interopérabilité entre ces deux systèmes de preuve formelle. Les théorèmes traduits sont fournis comme axiomes pour optimiser les performances.