The Coq mailing list

[Jacques Garrigue <garrigue AT math.nagoya-u.ac.jp>]

I see that you could find your file.

You can also have a look at my more recent scripts
  A Certified Implementation of ML with Structural Polymorphism
  http://www.math.nagoya-u.ac.jp/~garrigue/papers/
Unfortunately, they are for a much extended language, which means that they 
are much more complex.

Jacques Garrigue

On 2010/05/19, at 17:16, Roman Beslik wrote:

> Thanks. Can I get Coq source code? The link provided in the paper is 
> invalid.
> 
> On 19.05.10 10:44, 
>Â dubois AT ensiie.fr
>  wrote:
>> Hi
>> Yes there is one done 10 years ago. Look at the following paper
>> C. DUBOIS, V. MÉNISSIER-MORAIN.Certification of a type inference tool for 
>> ML: Damas-Milner within Coq. Journal of Automated Reasoning,Kluwer 
>> Academic Publishers, vol 23, No 3-4, 319-346
>> 
>> Catherine Dubois
>> ------Message d'origine------
>> De : Roman Beslik
>> À : Coq-Club
>> Objet : [Coq-Club] Hindley-Milner type inference algorithm
>> Envoyé : 19 mai, 2010 09:01
>> 
>> Hi all. Is there a formalization of the subject in Coq?
>>   
> 
> -- 
> Best regards,
>  Roman Beslik.
>