Boris Yakobowski

research and other interests


  author = {Didier Rémy and Boris Yakobowski},
  title = {A Church-style intermediate language for {MLF}},
  note = {Submitted},
  month = jul,
  year = 2009,
  url = {},
  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.}
  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 = {},
  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.  }
  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 = {},
  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.}
  author = {Boris Yakobowski},
  title = {Graphical types and constraints: second-order polymorphism
                  and inference},
  school = {University Paris 7},
  year = 2008,
  month = dec,
  url = {},
  pdf = {}
  author = {Boris Yakobowski},
  title = {Types et contraintes graphiques : polymorphisme de second
                  ordre et inférence},
  school = {Université Paris 7},
  year = 2008,
  month = dec,
  url = {},
  pdf = {}
  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 = {},
  publisher = {ACM Press},
  url = {},
  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.}
  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 = {},
  url = {},
  pdf = {},
  pdf-long = {},
  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.}
  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 = {},
  pdf = {}
  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 = {},
  pdf = {}
  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 = {},
  note = {In French}

Random photographs