I'm an assistant professor at EPFL. Previously, I was a PhD candidate at MIT with Adam Chlipala and then a senior applied scientist at Amazon AWS. My research focuses on programming languages, compilers, and formal verification; my broader interests include systems engineering, hardware design languages, security, performance engineering, databases, and type theory.
Prospective students: hi! Check out this dedicated page. I'm starting a new research group at EPFL and I have PhD positions open for Fall 2023.
Research
My current research program is organized around three main axes:
- Extensible compilation (teaching compilers domain-specific optimization tricks to compile high-level programs to very efficient low-level code),
- Hardware design languages and hardware verification (creating ways to describe and verify hardware and connect it to verified software to get end-to-end guarantees),
- Tooling for proof assistants (to support verification efforts, lower entry barriers, and democratize verification technology).
My faculty application research summary (pdf) had more info. The following are some concrete recent projects:
Correct-by-construction refinement
Fiat is a library for the Coq proof assistant that lets users automatically refine declarative specifications into efficient functional programs.
Narcissus is an extensible library of context-sensitive parser combinators, general enough to specify and automatically derive verified encoders and decoders for a wide range of binary formats like Ethernet, ARP, TCP, IP, etc.
Extensible proof-producing compilers and binary code extraction
F2F is a program extraction framework for Coq that uses syntax-driven automation to derive correct-by-construction imperative programs from nondeterministic functional source code.
Rupicola is a compiler-construction toolkit that lets users assemble verified domain-specific compilers from reusable translation lemmas, producing high-performance low-level code from unoptimized domain-specific functional models.
Hardware design languages: semantics and verification
Kôika is a rule-based hardware design language with cycle-accurate semantics formalized in Coq. It features high-level abstractions inherited from Bluespec, executable semantics proven to refine one-rule-at-a-time execution, and a formally-verified compiler that generates circuits with good performance.
Cuttlesim is a fast cycle-accurate simulator for Kôika that beats state-of-the-art RTL simulators by a factor 2 to 5 by leveraging high-level information to minimize redundant work. Cuttlesim generates C++ models that are readable enough to enable hardware debugging and testing using traditional software tools.
Tooling for interactive theorem provers
Alectryon is a literate-programming system for Coq that produces interactive visualizations of Coq proofs. Alectryon offers a new way to write, communicate, and preserve proofs, combining the flexibility of procedural proof scripts and the intelligibility of declarative proofs.
Selected publications
PLDIRelational Compilation for Performance-Critical Applicationspdf, bib
Proceedings of the ACM on Programming Languages (PLDI 2022).
ASPLOSEffective Simulation and Debugging for a High-Level Hardware Language using Software Compilerspdf, bib
Proceedings of the 26th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2021).
SLEUntangling Mechanized Proofspdf, bib
Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering (SLE 2020).
PLDIThe Essence of Bluespec: A Core Language for Rule-Based Hardware Designpdf, bib
Proceedings of the ACM on Programming Languages (PLDI 2020).
ICFPNarcissus: Correct-by-Construction Derivation of Decoders and Encoders from Binary Formatspdf, bib
Proceedings of the ACM on Programming Languages (ICFP 2019).
CAVTrigger Selection Strategies to Stabilize Program Verifierspdf, bib
Computer Aided Verification: 28th International Conference (CAV 2016).
POPLFiat: Deductive Synthesis of Abstract Data Types in a Proof Assistantpdf, bib
Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015).
Selected awards
Distinguished artifact, Untangling Mechanized Proofs, ACM SIGPLAN International Conference on Software Language Engineering (2020).
William A. Martin Memorial Thesis Award for Outstanding Thesis in CS, Compilation using Correct-by-Construction Program Synthesis, MIT (2016).
Frederick C. Hennie III Teaching Award in Recognition of Outstanding Contributions to Departmental Teaching, 6.009 Fundamentals of Programming, MIT (2016).
Service
AEC Co-chair: CAV 2021
PC member: PriSC'23, CoqPL'23, CPP'23, POPL'23, PLDI'22, LATTE'21, PLOS'21
Student PC member: IEEE S&P'19
Journal reviewer: NASA's Formal Methods Symposium, Journal of Statistical Computation and Simulation, Journal of Functional Programming
Conference volunteer: PLDI'18, SPLASH'18
Trivia and background
I'm originally from France. I did my undergrad at École Polytechnique, then moved to the US (MIT) for my PhD (all the details are in my CV). My MSc and PhD theses were both on proof-producing compilers.
I do a lot of software development. Some of it is still pretty popular on SourceForge, though most of my development activity happens on Github these days. Over time I've launched or contributed to a bunch of FLOSS projects , including plugins and translations for Rockbox (a free audio player firmware), documentation tools for Coq and F⋆, and Emacs packages for bibliography management, syntax checking, and various research languages (I wrote biblio.el, ESH, company-coq, F⋆-mode, and boogie-friends; I co-maintain Flycheck and Proof-General).
Apparently, some of my highest-cited writing is from my early-college blog.
For a while I was president of École Polytechnique's Japan student association, which mostly meant organizing movie showings and food tastings. Around that time I also learnt a lot of Chinese, and at some point made some money selling a Chinese-English dictionary for Windows Phone — it even had its own twitter feed.