5 Jun 2015
Joint work with Sandrine Blazy and David Bühler.
In this paper, we present a generic abstract interpretation based framework to enhance the precision of analyses on codes containing multiple successive conditionals. We introduce predicated domains, that preserve and reuse information valid only inside some branches of the code. Our predicates, derived from the conditional statements of the program, postpone the loss of information caused by joins.
This article has been published in the proceedings of FMICS 2014, where it was awarded the best paper award. Here are the pdf and the link at the publisher's website. A journal version is under consideration for publication.
15 Jul 2009
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.
19 May 2009
I have presented, during the Journées Francophones des Langages Applicatifs 2008, an article entitled Le caractère ` à la rescousse - Factorisation et réutilisation de code grâce aux variants polymorphes ("The ` character to the rescue - Code factorization and reuse using polymorphic variants", but the article is only available in french for the moment). It provides a hopefully gentle introduction to polymorphic variants, a feature of the typing system of OCaml.
The abstract and the BibTeX entry can be found on my publications page.
Three different presentations of this work are available (all three are in french)
1 Feb 2009
I have defended my PhD «Graphical types and constraints: second-order polymorphism and inference» on December 17th, 2008. The jury was composed of
|Pr. Stephanie Weirich||University of Pennsylvania|
|Pr. Fritz Henglein||University of Copenhagen|
|Roberto Di Cosmo||University Paris 7|
|Alexandre Miquel||University Paris 7, ENS Lyon|
|Didier Rémy (PhD advisor)||INRIA|
The final version of the manuscript can be found on TEL, or directly here in color or in black & white. There also exist fully english versions, in color and in black & white. BibTeX entries can be found on my publications page. The slides of the defense are also available.
22 Sep 2008
This paper, presented at ICFP'08, describes ML type inference in an entirely graphical setting, and shows that MLF type inference is only a very simple generalization of the ML case. Our approach is constraints-based; we give some equivalence rules on constraints, as well as an algorithm to solve them. We also show that type inference for MLF has linear complexity in practice, as in ML.
The full abstract for the paper can be found in my publications page. Compared to the published version, this version corrects some small mistakes in Definitions 9 and 11, and in Figure 17. The long version is available as Part 2 of my PhD dissertation.
Some talks I gave about this work:
1 Feb 2008
2 Dec 2007
15 Nov 2007
1 Oct 2007
Nice titles have became hugely popular, and many people proposed variants. I will mention those of Dunstan Orchard and Mark Wubben. This entry presents yet another implementation, with some features found only in some of the above versions, and some entirely new. I've also corrected what I believed to be bugs.
What's in this version?
- The nicetitles follow the mouse.
- The size of the nicetitles is not fixed. This avoids some overflow problems when their content is too big.
- The nicetitles do not go outside of the window, and they try moderately hard not to appear on top of the mouse cursor.
- The nicetitles appear after a little delay (and e.g.
‘sup’tags inside the text of the anchors do not cause delays).
- Nicetitles can be used to display image thumbnails. Currently,
‘img’tags with the
‘thumb’class automatically receive thumbnails; see the photographs on the right.
- The code is thoroughly tested under various versions of Gecko, Internet Explorer (versions 6 and 7), Opera (versions 8 and 9), Konqueror and Safari 3 (for Windows).
The source code is available, as a
.js file or
You also need to add inside the file an implementation of
addEvent function that correctly handles the scopes
‘this’ keyword. I currently use
stylesheet I use on this site can be used as an example to format
the nicetitles boxes.
I am interested to hear about any problem encountered while using this code. My mail can be found on this page, should you wish to contact me.
- 2007-10: fixed a bug in Safari
8 May 2007
18 Jan 2007
10 Sep 2006
Alain Frisch has created a webpage about our participation to the 2006 ICFP programming contest. This year's problems were quite varied, and my main contribution was to solve the raytracer subproblem.
The raytracer had to be written in a langage where functions are 2D boxes composed of wires. Those wires link atomic boxes that themselves perform operations of construction and deconstruction on completely untyped objects. I wrote an ML solution to the problem (this was in itself non-trivial), and we compiled it into a 2D function using code written by Alain and Nicolas.
The main peculiarity of my solution is that it is typed, even though it dutifully follows the untyped representation of the specification. I used polymorphic variants, which enabled me to define the type (for example) of ray-tracing values or of lists as subtypes of the generic value type.
type value = [ | `Unit | `Pair of value * value | `Inl of value | `Inr of value ] type valrt = [ `Inl of u | `Inr of [ `Inl of u | `Inr of [`Inl of u]]] type 'a vlist = [ `Inl of [`Pair of 'a * 'b] | `Inr of [`Unit] ] as 'b
28 Oct 2005
In ML-based languages, the construction
let x = e in e'
is equivalent, at execution-time, to
(fun x -> e') e.
However this property does not hold during type-checking: the
let construct permits to generalize the type variables
which are free in the environment; this way, more polymorphism can be
Consequently, it is potentially helpful to replace all applications by
let bindings. In OCaml, this can be done automatically by Camlp4 (this
patch is intended for OCaml 3.09; otherwise, change
To compile a
cmo usable as a parser by Camlp4, use
ocamlc -I +camlp4 -pp "camlp4r pa_extend.cmo q_MLast.cmo" -c pa_o_let_extend.ml.
You can create an extended Camlp4 executable by using
mkcamlp4 -o $(CAMLP4LET) pa_o.cmo pa_o_let_extend.cmo pr_o.cmo
(for a Camlp4 accepting the original syntax as input).
25 Sep 2004
As we guessed (we were warned in advance that we had won a prize, and the performances of our ants seemed too low to win one of the first two prizes), we have won the Judge's Prize of the ICFP Programming Contest 2004. As expected, we received the prize thanks to the design of our intermediate language (the ultimate goal was to compile ant brains) ; the compiler was mainly due to Xavier Leroy, with additions from Damien Doligez and myself.