Rauber Du Bois, A.; Ribeiro, R.; Amaro, M. A Mechanized Proof of a Textbook Type Unification Algorithm. RITA 2020, 27, 13-24.