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 ...
Research Assistant
AI chat, annotations, notes & similar papers
No comments yet
Be the first to share your thoughts!