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 ...
We describe a formalization of the elementary algebra, topology and analysis of finite-dimensional Euclidean space in the HOL Light theorem prover. (Euclidean space is RN with the...