Boris Yakobowski

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.

The work has been integrated into Frama-C as a new plugin. Experiments on real code show that our approach scales, and improves significantly the precision of the Value Analysis plugin of Frama-C.

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.

Coq proofs of the results in the journal version: .v file, or as an html page.

Didier Rémy and I have written an article completing the ML^F "trilogy", entitled A Church-style intermediate language for ML^F. We describe an explicit language for a lambda-calculus with (ML^F-style) flexible quantification; the language, called xML^F, extends the explicit version of System F with a new form of type applications. Using xML^F, it becomes possible to use ML^F in a compiler that uses a typed intermediate language. We describe how to elaborate the results of the (graphical) ML^F type inference algorithms into xML^F terms.

The article is currently submitted for publication; a preliminary version is available here. See also those slides (2009-02-09, Gallium seminar, in english), or those of Didier Rémy's talk at IFIP.

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.

Here is the source code of the examples: introduction, section 2, section 3 and section 4.

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)

• 2008-21-01, Gallium seminar
• 2008-28-01, JFLA
• 2009-05-19, CEA

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
Hugo Herbelin	INRIA
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.

This paper, presented at ICFP'08, describes ML type inference in an entirely graphical setting, and shows that ML^F 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 ML^F 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:

• 2008-09-22 ICFP 2008
• 2008-02-11 Gallium seminar (in french, slightly outdated)

A proof-of-concept prototype implementation of an ML^F typer, based on the results presented in our last paper, is online, and has been slightly updated. The source code is now also available.

Didier Rémy and I have written a paper on a graph-based presentation of the types of the ML^F 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.

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.

The slides I've used are here in pdf, or there for Advi users (the Advi version contains more transitions, but needs some manual recentering).

Note that all the content presented in the extended abstract is developped in this article.

The subject of my PhD Thesis is now online. It is entitled (in french) « Polymorphisme d'ordre omega avec inférence partielle mis en pratique »; I'm going to extend Didier Rémy and Didier Le Botlan's MLF.

I've defended today my Master Thesis, about certified compilation using an intermediate language in SSA form. The report and the slides I've presented are available, in pdf (in french only).

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).

I have presented the paper at LOPSTR'04 in Verona, Italy. The slides I used are here; you need advi to view them.

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.