The Coq mailing list

[Yannick <yannick_duchene AT yahoo.fr>]

On Mon, 19 Mar 2012 15:32:52 +0100, Xavier Leroy <Xavier.Leroy AT inria.fr>  
wrote:

> On 03/16/2012 09:11 AM, Jacques Garrigue wrote:
>
> > Extraction to Ada seems another problem: how do you encode the
> > lambda-calculus in Ada?
>
> Painfully :-)  See:
>
> "From ML to Ada: Strongly-typed Language Interoperability via Source
> Translation", A. Tolmach and D. Oliva. Journal of Functional
> Programming, 8(4),367-412, July 1998.
>
> http://web.cecs.pdx.edu/~apt/jfp98.ps
>
> - Xavier Leroy

Seems good. If you know other papers of the like, please, let me know  
(well, "let us know").

--
Yannick Duchêne