Importing HOL Light into Coq

Abstract. We present a new scheme to translate mathematical developments from HOL Light to Coq, where they can be re-used and rechecked. By relying on a carefully chosen embedding of Higher-Order Logic into Type Theory, we try to avoid some pitfalls of inter-operation between proof systems. In particular, our translation keeps the mathematical statements intelligible. This translation has been implemented and allows the importation of the HOL Light basic library into Coq.

• Type: Conference
• Year: 2010
• Where: ITP
• Authors: Chantal Keller, Benjamin Werner
• Keywords: HOL Light, ITP 2010, Light Basic Library, Mathematical Developments, Mathematics