{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T14:30:47Z","timestamp":1759847447100},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We present a method and a tool, hol2dk, to fully automatically translate proofs from the proof assistant HOL-Light to the proof assistant Coq, by using Dedukti as an intermediate language. Moreover, a number of types, functions and predicates defined in HOL-Light are proved (by hand) to be equal to their counterpart in the Coq standard library. By replacing those types and functions by their Coq counterpart everywhere, we obtain a library of theorems (based on classical logic like HOL-Light) that can directly be used and applied in other Coq developments.<\/jats:p>","DOI":"10.29007\/6k4x","type":"proceedings-article","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T22:10:10Z","timestamp":1716847810000},"page":"1--18","source":"Crossref","is-referenced-by-count":4,"title":["Translating HOL-Light proofs to Coq"],"prefix":"10.29007","volume":"100","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Blanqui","sequence":"first","affiliation":[]}],"member":"11545","event":{"name":"Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T22:10:13Z","timestamp":1716847813000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/mtFT"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/6k4x","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}