@inproceedings{b0f282cba50b4a90b11033284e528b91,
title = "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 re-checked. 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.",
author = "Chantal Keller and Benjamin Werner",
year = "2010",
month = jan,
day = "1",
doi = "10.1007/978-3-642-14052-5\_22",
language = "English",
isbn = "3642140513",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "307--322",
booktitle = "Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings",
note = "1st International Conference on Interactive Theorem Proving, ITP 2010 ; Conference date: 11-07-2010 Through 14-07-2010",
}