Carneiro, M. M. Conversion of HOL Light Proofs into Metamath. JFR 2016, 9, 187-200.