C. Dubois, V. Ménissier‑Morain : “A Proved Type Inference Tool for ML: Damas-Milner within Coq”, Proceedings of the9-thth International Conference on Theorem Proving in Higher Order Logics, TUCS General Publication, J. von Wright, J. Grundy, J. Harrison (Eds.), http://www.tucs.abo.fi/cgi-bin/getps.cgi/publications/general/, pp. 15-30 [Dubois 1996]