© Xavier Pierre / CNRS
I am a CNRS researcher in the CAMUS / ICPS team of ICube, in Strasbourg, France. The goal of my research is to empower programmers to optimize programs safely, interactively, and across abstraction layers. In particular, I am one of the lead contributors to OptiTrust, a framework for programmer-guided, verified program optimization, based on source-to-source transformations and separation logic. OptiTrust is led by Arthur Charguéraud. Check out some OptiTrust case studies here.
Building up on OptiTrust, I plan to develop a novel optimization assistant that adapts to software and hardware evolution, includes an effective interactive feedback loop, and is able to reason about numerical accuracy of finite precision numbers (integers, floating-point and fixed point numbers). I am open to collaborations and regularly looking for motivated students interested in becoming young researchers!
I received my PhD from the School of Computing Science at the University of Glasgow, in Scotland, supervised by Michel Steuwer and Phil Trinder. I worked on the high-level functional language Rise and its Shine compiler that applies optimizations using rewrite rules before generating imperative code. My thesis shows the potential of Shine to achieve domain-extensibility, controllable automation, and generate high performance code. Domain-extensibility facilitates adapting compilers to new algorithms and hardware. Controllable automation enables performance engineers to gradually take control of the optimization process.
You can read my Curriculum Vitae to learn more.