The Coq mailing list

[Roman Beslik <beroal AT ukr.net>]

So I have found this file:
http://www-calfor.lip6.fr/~vmm/documents/proof_VMM_CD.tar.gz
{{{
             Certification of a type inference tool for ML
             Catherine Dubois and Valérie Ménissier-Morain
    Universite d'Evry, specif research team and GIE Dyade, VIP action
-------------------------------------------------------------------------------

This tar file contains a description and a proof of correctness for
the W algorithm to synthesize the principal type of an ML expression.
}}}
On 19.05.10 11:42, 
dubois AT ensiie.fr
 wrote:
> I can send you the code next week. I am out my lab during all the week and I 
> would like to verify everything is still ok
>    

--
Best regards,
  Roman Beslik.