Boris Yakobowski

research and other interests


15 Jul 2009

xMLF, a Church-style intermediate language for MLF

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

Random photographs