Lazy strategies
I'm working with Delia Kesner on various aspects of optimal reduction in the framework of weak reduction, and on the sharing of subterms. Some of my targets are: the lambda-calculus, higher-order rewriting, and pattern matching calculi. I also study how weak reduction gives to higher-order rewriting a "first-order" behavior.
Documents
- A paper on optimal reduction in the weak lambda-calculus (ICFP, september 2013).
- My PhD dissertation (in french), and the slides used for the defense.
- A paper on an axiomatic approach to the sharing of subterms in abstract rewriting (RTA, may 2012).
- A paper on full laziness and fully lazy lambda-lifting (POPL, january 2012). See also the slides from talks at CHoCoLa, LAC-GEOCAL, PoPL.
- A set of slides on optimal sharing for weak reduction in higher-order rewriting (Vrije Universiteit Amsterdam, January 2011).
Pattern matching-oriented calculi
Exploring the weirdnesses of the evaluation of pattern matching, especially when the patterns are dynamic or when we give up Berry's stability property.
Documents
- A set of slides and a paper on optimal sharing and weak reduction (PPDP, july 2010).
- A set of slides and a paper on explicit pattern matching and reduction strategies (HOR, july 2010).
Weak memory concurrency and optimisation of C11 programs
In this work we are considering the relaxed memory model for concurrency of the C11/C++11 standard, and characterizing families of optimisations that are sound with respect to the low-level atomics of C11 and their synchronization effects.
This is joint work with Francesco Zappa Nardelli and Robin Morisset from ENS, and Viktor Vafeiadis and Soham Chakraborty from MPI-SWS.
Documents
- A paper on the program transformations that are (dis-)allowed by the C11 standard, and some tentative fixes to the standard.
- The page of this project (including the Coq development).
- This work also participates in a more general investigation on weak memory concurrency.
Separation logic and data races
The language Mezzo is a programming language in the ML tradition, which places strong emphasis on the control of aliasing and access to mutable memory. Its type system can be thought of as "Reynold's separation logic turned into a type system".
The language has been designed by François Pottier and Jonathan Protzenko, and I participated in baking shared-memory concurrency into the kernel of Mezzo, and proving the soundness of its type system in the Coq proof assistant.
Documents
- A general paper describing the design and the formalization of Mezzo, submitted for publication.
- A paper describing concurrency in Mezzo and the formalization of a fragment of the language, and proving the absence of data races in well-typed programs (FLOPS, june 2014).
- Coq development (take 2, cleaner) of the formalization of the fragment presented in the paper.
- Coq development (take 1, complete) of the full formalization of the type system of Mezzo.
Geometric interpretation of concurrency
Collaboration with Emmanuel Haucourt on the analysis of independence of processes in a concurrent program by geometrical means.