M. M. Carneiro, “Conversion of HOL Light proofs into Metamath”, JFR, vol. 9, no. 1, pp. 187–200, Jan. 2016.