TY - RPRT TI - Aligning HOL-Light and Rocq libraries formally AU - Frédéric Blanqui AU - Antoine Gontard PY - 2026 UR - https://arxiv.org/abs/2609.24598 ID - 2609.24598 ER -