Rauber Du Bois, A., R. Ribeiro, and M. Amaro. “A Mechanized Proof of a Textbook Type Unification Algorithm”. Revista De Informática Teórica E Aplicada, vol. 27, no. 3, June 2020, pp. 13-24, doi:10.22456/2175-2745.100968.