@Unpublished{Remy-Yakobowski/mlf-graphic-types,
  AUTHOR =       "Didier R{\'e}my and Boris Yakobowski",
  TITLE =        "A graphical presentation of {\MLF} types with
                  a linear-time incremental unification algorithm.",
  url  =     {http://pauillac.inria.fr/~remy/publications.html#Remy/mlf-graphic-types},
  html  =    {http://pauillac.inria.fr/~remy/work/mlf},
  psgz =     {http://pauillac.inria.fr/~remy/work/mlf/mlf-graphic-types.ps.gz},
  pdf =      {http://pauillac.inria.fr/~remy/work/mlf/mlf-graphic-types.pdf},
  YEAR =      2006,
  MONTH =     sep,
  ABSTRACT = {
MLF is a language that extends both ML and System F and combines the
benefits of both. We propose a dag representation of MLF types that
superposes a term-dag, encoding the underlying term-structure with
sharing, and a binding tree, encoding the binding-structure. This
representation is more canonical as it factors out most of the
notational details of the original definition; it is also closely
related to first-order terms. Moreover, it permits a simpler and more
direct definition of type instance that combines type-instance on
first-order term-dags, simple operations on dags, and a control that
allows or rejects potential instances. Thanks to this representation, we
obtain an incremental linear-time unification algorithm for MLF types,
which we prove sound and complete with respect to the specification.
  We also extend term graphs to express constraints on graphs that can
be rewritten incrementally, which suffices to describe all operations
needed by type inference. 
}
}

@Unpublished{Remy-Yakobowski/mlf-graphic-types-long,
  AUTHOR =       "Didier R{\'e}my and Boris Yakobowski",
  TITLE =        "A graphical presentation of {\MLF} types with
                  a linear-time incremental unification algorithm.",
  url  =     {http://pauillac.inria.fr/~remy/work/mlf},
  html  =    {http://pauillac.inria.fr/~remy/work/mlf},
  psgz =     {http://pauillac.inria.fr/~remy/work/mlf/mlf-graphic-types-long.ps.gz},
  pdf =      {http://pauillac.inria.fr/~remy/work/mlf/mlf-graphic-types-long.pdf},
  YEAR =      2006,
  MONTH =     sep,
  NOTE = {{Extended} version, available at \url{http://pauillac.inria.fr/~remy/work/mlf}},
  ABSTRACT = {
MLF is a language that extends both ML and System F and combines the
benefits of both. We propose a dag representation of MLF types that
superposes a term-dag, encoding the underlying term-structure with
sharing, and a binding tree, encoding the binding-structure. This
representation is more canonical as it factors out most of the
notational details of the original definition; it is also closely
related to first-order terms. Moreover, it permits a simpler and more
direct definition of type instance that combines type-instance on
first-order term-dags, simple operations on dags, and a control that
allows or rejects potential instances. Thanks to this representation, we
obtain an incremental linear-time unification algorithm for MLF types,
which we prove sound and complete with respect to the specification.
  We also extend term graphs to express constraints on graphs that can
be rewritten incrementally, which suffices to describe all operations
needed by type inference. 
}
}
%  NOTE = {Extended version of \cite{Remy-Yakobowski/mlf-graphic-types}},