ML^F

This project is joint work with Didier Le Botlan, Boris Yakobowski, Paolo Herms, and Gabriel Scherer.

Prototypes

A new proptype of MLF is under implementation here.

See also the old prototype by Boris Yakobowski,

MLF-omega (new)

Partial Type Inference with Higher-Order Types.

Preliminary investigation was conducted by Paolo Hemrs in his master dissertation. [ PDF | BIB ]. Further invertigation has been done by Gabriel Scherer [ PDF | BIB ]. This has been implemented in the new prototype.

The calculus

A Church-Style Intermediate Language for MLF

This is joint work with Boris Yakobowski.

An extended abstract [ ABSTRACT | PDF | BIB ] introduces the intermediate language xMLF and describes an elaboration of eMLF into xMLF. The journal version [ ABSTRACT | PDF | BIB ] will appear in TCS. See alse this talk [ ABSTRACT | PDF ] given at IFIP WG 2.8.

Parts of the metatheory of xMLF have been mechanically verified in Coq in this Coq development by Boris Yakobowski.

The elaboration has been implemented in this prototype Gabriel Scherer.

The graphical presentation

This is joint work with Boris Yakobowski.

Boris Yakobowski's PhD dissertation

Boris' dissertation covers graphical types and constraints, graphical type inference, described below, and the Church-Style intermediate Language for MLF [ URL | PDF ].

Graphic Type Constraints and Efficient Type Inference: from ML to ML^F.

This describes the generalization of graphical types to typing constrainst and their application to type inference. The work has been presented at ICFP 08 [ PDF | ABS | BIB ]. (This version fixes two small errors from the proceeding version.) You may also see an earlier extended version. and those those slides and try the online prototype.

A graphical representation of ML^F types with a linear-time incremental unification algorithm.

This works describes graphical types and their application to unification. It has been presented at the conference TLDI 07 [ ABSTRACT | PDF | BIB ]

The recast version

Recasting ML^F

This is joint work with Didier Le Botlan. appeared in Information and Computation Volume 207, Issue 6, June 2009, Pages 726-785 also available as INRIA Research Report 6228.

The Original

ML^F: Raising ML to the Power of System-F

This is the initial joint work with Didier Le Botlan. This work has been presented at the Conference (ICFP 03).

ML^F: Une extension de ML avec polymorphisme de second ordre et instanciation implicite.

This is Didier Le Botlan's PhD dissertation, which is available both in English [ mlf.dvi.gz | mlf.ps.gz | mlf.pdf | mlf.bib ] and in French. See also examples on Didier Le Botlan's page.

Talks

A new look at ML^F.

Talk given at Portland State University, June 2008 [ PDF ].

ML^F for Everyone (Users, Implementers, and Designers).

Invited talk given at the ML 2007 workshop [ PDF ].

Older slides

• Graphic type constraints, IFIP workshop, Iceland, 2007 [ PDF ].
• Graphical types, IFIP workshop, 2006 [ PDF ].