I'm an assistant professor at EPFL, heading the SYSTEMF lab. 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, and type theory.
Prospective students: hi! Check out this dedicated page and my lab's website.
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:
Formal methods for real-world DSLs
Elk is a linear-time engine for a subset of JavaScript regular expressions (regexes). Some of the algorithms pioneered in Elk have been merged into V8 (and hence Chrome and Node.js).
Warblre is a near-complete Coq translation of the JS regex specification. Developing this spec helped us find mistakes in previous paper-based specifications and disprove longstanding assumptions about JS regexes.
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
ICFPA Coq Mechanization of JavaScript Regular Expression Semanticspdf, bib
Proceedings of the ACM on Programming Languages (ICFP 2024).
PLDILinear Matching of JavaScript Regular Expressionspdf, bib
Proceedings of the ACM on Programming Languages (PLDI 2024).
PLDIFoundational Integration Verification of a Cryptographic Serverpdf, bib
Proceedings of the ACM on Programming Languages (PLDI 2024).
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).
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
Events: PLDI'24-25 (Workshops and tutorials chair), Coq Workshop'24 (PC chair), Proof Systems'24 (Organizer), POPL'24 (Session previews chair), Swiss Verification Day'24 (Organizer), CAV'21 (AEC chair)
Reviewing: OOPSLA'25, OSDI'25, CPP'25, POPL'25, HATRA'24, SEFI'24, ICFP'24, ESOP'24, PLDI'24, SPLASH'23 SRC, APLAS'23, CPP'23, CoqPL'23, LATTE'23, POPL'23, PriSC'23, PLDI'22, Coq Workshop'22, LATTE'21, PLOS'21, Formal Methods Symposium, Journal of Statistical Computation and Simulation, Journal of Functional Programming
Invited speaker: CoqPL'22
Session chair: ICFP'24 (Verification and Cost Analysis), PLDI'24 (Verification II), POPL'24 (Session preview), PLDI'22 (Hardware I, Memory), SPLASH'21 (SIGPLAN)
SRC judge: PLDI'24
Mentor: PLATEAU'24, PLATEAU'23
Student PC member: IEEE S&P'19
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, Lean and F⋆, and Emacs packages for bibliography management, on-the-fly 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).
For a while, some of my highest-cited writing was 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.