Carneiro, Mario M. “Conversion of HOL Light Proofs into Metamath”. Journal of Formalized Reasoning 9, no. 1 (January 1, 2016): 187–200. Accessed April 26, 2024. https://jfr.unibo.it/article/view/4596.