@unpublished{BY-xmlf,
author = {Didier Rémy and Boris Yakobowski},
title = {A Church-style intermediate language for {MLF}},
note = {Submitted},
month = jul,
year = 2009,
url = {http://www.yakobowski.org/xmlf.html},
pdf = {http://www.yakobowski.org/publis/2009/xmlf.pdf},
abstract = {MLF is a type system that seamlessly merges ML-style
implicit but second-class polymorphism with System F
explicit first-class polymorphism. We present xMLF,
a Church-style version of MLF with full type
information that can easily be maintained during
reduction. All parameters of functions are
explicitly typed and both type abstraction and type
instantiation are explicit. However, type
instantiation in xMLF is more general than type
application in System F. We equip xMLF with a
small-step reduction semantics that allows reduction
in any context and show that this relation is
confluent and type preserving. We also show that
both subject reduction and progress hold for
weak-reduction strategies, including the
call-by-value with the value-restriction. We exhibit
a type preserving encoding of MLF into xMLF, which
ensures type soundness for the most general version
of MLF. We observe that xMLF is a calculus of
retyping functions at the type level.}
}
@inproceedings{BY-variants-polymorphes,
author = {Boris Yakobowski},
title = {Le caractère ` à la rescousse - Factorisation et
réutilisation de code grâce aux variants polymorphes},
booktitle = {JFLA 2008 - Dix-neuvièmes Journées Francophones
des Langages Applicatifs},
year = 2008,
month = jan,
address = {Étretat},
pages = {63-77},
isbn = {2-7261-1295-11},
publisher = {INRIA},
url = {http://www.yakobowski.org/jfla08.html},
pdf = {http://www.yakobowski.org/publis/2008/jfla08.pdf},
abstract = {Les variants polymorphes sont une fonctionnalité
puissante du système de types du langage OCaml, dont
l'utilisation reste pourtant rare. Dans cet article,
nous nous attachons à montrer en quoi ils sont plus
expressifs que les types inductifs usuels, à la fois
en terme de garantie statique d'invariants et de
factorisation de code. Pour cela, nous proposons
trois exemples tirés d'un typeur. Aucune
connaissance préalable sur les variants polymorphes
n'est nécessaire. }
}
@inproceedings{Remy-Yakobowski-mlfc,
author = {Didier Rémy and Boris Yakobowski},
title = {From {ML} to {MLF}: Graphic Type Constraints with Efficient
Type inference},
year = 2008,
month = sep,
booktitle = {Proceedings of the 13th ACM SIGPLAN International
Conference on Functional Programming (ICFP'08),
Victoria, British Columbia, Canada},
pages = {63-74},
publisher = {ACM Press},
url = {http://www.yakobowski.org/research.html#mlfc},
pdf = {http://www.yakobowski.org/publis/2008/mlf-type-inference-icfp08-corrected.pdf},
abstract = {MLF is a type system that seamlessly merges
ML-style type inference with System-F
polymorphism. We propose a system of graphic (type)
constraints that can be used to perform type
inference in both ML or MLF. We show that this
constraint system is a small extension of the
formalism of graphic types, originally introduced to
represent MLF types. We give a few semantic
preserving transformations on constraints and
propose a strategy for applying them to solve
constraints. We show that the resulting algorithm
has optimal complexity for MLF type inference, and
argue that, as for ML, this complexity is linear
under reasonable assumptions.}
}
@phdthesis{BY-PhD-en,
author = {Boris Yakobowski},
title = {Graphical types and constraints: second-order polymorphism
and inference},
school = {University Paris 7},
year = 2008,
month = dec,
url = {http://www.yakobowski.org/phd-dissertation.html},
pdf = {http://www.yakobowski.org/publis/2008/these-finale.pdf}
}
@phdthesis{BY-PhD,
author = {Boris Yakobowski},
title = {Types et contraintes graphiques : polymorphisme de second
ordre et inférence},
school = {Université Paris 7},
year = 2008,
month = dec,
url = {http://www.yakobowski.org/phd-dissertation.html},
pdf = {http://www.yakobowski.org/publis/2008/these-finale-francais.pdf}
}
@inproceedings{BY-mlfg,
author = {Didier Rémy and Boris Yakobowski},
title = {A graphical presentation of {MLF} types with a
linear-time unification algorithm},
booktitle = {TLDI'07: Proceedings of the 2007 ACM SIGPLAN
International Workshop on Types in Languages Design
and Implementation},
year = 2007,
isbn = {1-59593-393-X},
pages = {27--38},
address = {Nice, France},
month = jan,
url-publisher = {http://doi.acm.org/10.1145/1190315.1190321},
publisher = {ACM Press},
url = {http://www.yakobowski.org/tldi07.html},
pdf = {http://www.yakobowski.org/publis/2007/mlfg-tldi2007-color.pdf},
abstract = {MLF is a language that extends 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. Compared to the original
definition, this representation is more canonical as
it factors out most of the notational details; 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. Using this representation, we build a
linear-time unification algorithm for MLF types,
which we prove sound and complete with respect to
the specification.}
}
@inproceedings{BY-term-enumeration-LOPSTR2004,
author = {J. B. Wells and Boris Yakobowski},
title = {Graph-Based Proof Counting and Enumeration with
Applications for Program Fragment Synthesis},
booktitle = {LOPSTR 2004: 14th International Symposium on Logic
Based Program Synthesis and Transformation, {LOPSTR}
2004, Verona, Italy, August 26-28, 2004, Revised
Selected Papers},
editor = {Sandro Etalle},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 3573,
year = 2005,
isbn = {3-540-26655-0},
pages = {262-277},
url-publisher = {http://dx.doi.org/10.1007/11506676_17},
url = {http://www.yakobowski.org/lopstr04.html},
pdf = {http://www.yakobowski.org/publis/2005/term-enumeration-final.pdf},
pdf-long = {http://www.yakobowski.org/publis/2004/term-enumeration.pdf},
abstract = {For use in earlier approaches to automated module
interface adaptation, we seek a restricted form of
program synthesis. Given some typing assumptions
and a desired result type, we wish to automatically
build a number of program fragments of this chosen
typing, using functions and values available in the
given typing environment. We call this problem
\emph{term enumeration}. To solve the problem, we
use the Curry-Howard correspondence
(propositions-as-types, proofs-as-programs) to
transform it into a \emph{proof enumeration} problem
for an intuitionistic logic calculus. We formally
study proof enumeration and counting in this
calculus. We prove that proof counting is solvable
and give an algorithm to solve it. This in turn
yields a proof enumeration algorithm.}
}
@inproceedings{BY-APPSEM05,
author = {Dider Rémy and Boris Yakobowski},
title = {{MLF} with Graphs},
booktitle = {APPSEM'05: Proceedings of the 3rd-APPSEM II Workshop
on Applied Semantics},
address = {Frauenchiemsee, Germany},
year = 2005,
month = sep,
note = {Extended abstract},
url = {http://www.yakobowski.org/appsem05.html},
pdf = {http://www.yakobowski.org/publis/2005/abstract-appsem-2005.pdf}
}
@mastersthesis{BY-semantique-SSA-DEA,
author = {Boris Yakobowski},
title = {{\'E}tude s\'emantique d'un langage interm\'ediaire
de type {S}tatic {S}ingle {A}ssignment},
school = {ENS Cachan and INRIA Rocquencourt},
year = 2004,
type = {Rapport de DEA ({M}aster's thesis)},
month = sep,
note = {In french},
url = {http://www.yakobowski.org/dea.html},
pdf = {http://www.yakobowski.org/publis/2004/rapport-dea.pdf}
}
@inproceedings{BY-module-matching-WIT2002,
author = {Boris Yakobowski},
title = {Module matching modulo isomorphisms},
booktitle = {WIT 2002, 1st International Workshop on Isomorphisms
of Types},
address = {Toulouse, France},
month = nov,
year = 2002,
publisher = {Electronic proceedings at
\url{http://www.irit.fr/zeno/WIT2002/}},
url = {http://www.yakobowski.org/wit02.html},
note = {In French}
}
