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:
9 Apr 2008
16 Jan 2007
Didier Rémy and I have written a paper on a graph-based presentation of the types of the MLF language. This paper has been presented at the TLDI'07 workshop. The submitted version of the paper (with a few typos corrected) is available, as well as a black and white version, and the slides I presented at the workshop.
Since its publication, we have made some important revisions to this work. A much developed version is available as Part 1 of my PhD dissertation.
The abstract of the paper, as well as a BibTeX entry, can be found in my publications page.
This work is the continuation of what I presented at the APPSEM II Workshop, and entirely supersedes it.
15 Sep 2005
I've presented at the 3rd APPSEM II Workshop a talk about some preliminary results of my thesis. More precisely, they consist in a reformulation of MLF using graphs for the representation of types. This is the corresponding extended abstract.
Note that all the content presented in the extended abstract is developped in this article.
28 Sep 2004
13 Sep 2004
28 Aug 2004
Using the resultas of an internship I did in the Ultra Group, Joe Wells and I have written a paper entitled « Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis », which was submitted to LOPSTR'04 (this is the version found in the preliminary proceedings of the conference).
A final version of the paper is also available. Please note that the preliminary one is slightly more complete, as it includes an appendix not found in the final paper.
Finally, the abstract of the paper can be found in my publications page.