Boris Yakobowski

Didier Rémy and I have written an article completing the ML^F "trilogy", entitled A Church-style intermediate language for ML^F. We describe an explicit language for a lambda-calculus with (ML^F-style) flexible quantification; the language, called xML^F, extends the explicit version of System F with a new form of type applications. Using xML^F, it becomes possible to use ML^F in a compiler that uses a typed intermediate language. We describe how to elaborate the results of the (graphical) ML^F type inference algorithms into xML^F terms.

The article is currently submitted for publication; a preliminary version is available here. See also those slides (2009-02-09, Gallium seminar, in english), or those of Didier Rémy's talk at IFIP.