Certification of a type inference tool for ML: Damas-Milner within Coq
scientific article; zbMATH DE number 1394792