coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq, SML and Ada

From: Xavier Leroy <Xavier.Leroy AT inria.fr>
To: Jacques Garrigue <garrigue AT math.nagoya-u.ac.jp>
Cc: yannick_duchene AT yahoo.fr, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Coq, SML and Ada
Date: Mon, 19 Mar 2012 15:32:52 +0100

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

[Coq-Club] Coq, SML and Ada, yannick_duchene
- Re: [Coq-Club] Coq, SML and Ada, Nuno Gaspar
- Re: [Coq-Club] Coq, SML and Ada, Jacques Garrigue
  - Re: [Coq-Club] Coq, SML and Ada, Xavier Leroy
    - Re: [Coq-Club] Coq, SML and Ada, Yannick
  - Re: [Coq-Club] Coq, SML and Ada, Pierre Letouzey