I'm a PhD candidate at MIT working in Adam Chlipala's lab. My research focuses on programming languages, extensible compilers, and verification; my broader interests include systems engineering, hardware design languages, security, optimization, databases, and type theory. I host free software on SourceForge and GitHub. Check out my blog, read my papers, say hi on twitter, or shoot me an email!
I'm applying for faculty positions this year! My application materials are available online.
Research 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.
Education
Massachusetts Institute of Technology (Cambridge, MA, USA)
MS 2016, PhD ongoing
PhD thesis: Modular proof-producing extraction for end-to-end verification.MS thesis: Compilation using Correct-by-Construction Program Synthesis. Minor: Corporate Finance. Modules include: Computational biology, Databases, Computer Architecture, Advanced Complexity Theory.Advised by Adam Chlipala.
École Polytechnique (Palaiseau, France)
Diplôme d'ingénieur 2014, MSE 2016
MSE specializing in computer science; undergraduate in mathematics and physics.GPA: 3.95. Modules include randomized algorithms, computer-aided reasoning, networking, algorithm design, compilation, information theory, differential geometry, harmonic analysis, dynamical systems, economy, and molecular biology.Served as student representative for the CS curriculum.
Lycée Louis-le-Grand (Paris, France)
Classes préparatoires, MP Info
Specialization in Mathematics and Physics.Served as elected class representative.
Selected publications
ASPLOSEffective Simulation & Debugging for High-Level Hardware Languages 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).
IJCARExtensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofspdf, bib
International Joint Conference on Automated Reasoning (IJCAR 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).
SNAPLThe End of History? Using a Proof Assistant to Replace Language Design with Library Designpdf, bib
2nd Summit on Advances in Programming Languages (SNAPL 2017).
CAVTrigger Selection Strategies to Stabilize Program Verifierspdf, bib
Computer Aided Verification: 28th International Conference (CAV 2016).
CoqPLCompany-Coq: Taking Proof General one step closer to a real IDEpdf, bib
The Second International Workshop on Coq for PL (CoqPL 2016).
Workshop paper.
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).
Teaching experience
Massachusetts Institute of Technology
Designed labs, taught recitations, prepared debriefings for MIT's Fundamentals of Programming class (6.009); received 65 student reviews with an average teaching rating of 6.8/7 and 55 perfect teaching scores, and was awarded a Frederick C. Hennie III Teaching Award in Recognition of Outstanding Contributions to Departmental Teaching.
4 month teaching assistantship
École Polytechnique
Volunteered as an English tutor, coaching classmates at École Polytechnique in one-on-one sessions to improve their English.
6 months teaching assignment
Association Tremplin
Designed AP-level mathematics, physics, and computer science classes and taught over 60 motivated teenagers across three high schools from low-income neighborhoods. Classes were intended to encourage college applications, boost student confidence, and increase preparedness. Over 95% of the students completed the program successfully.
7 months civil service in Seine-Saint-Denis, France
Research & industry experience
INRIA (Prosecco team, supervised by Cătălin Hriţcu)
Implemented reflective pattern-matching tactics for F⋆; contributed to research on effect erasure; rewrote F⋆'s IDE protocol and state machine to implement a full-fledged IDE; built a literate programming system for F⋆; assembled web-based builds of F⋆ and Z3.
3 months internship in Paris, France
Microsoft Research (RISE group, supervised by K. Rustan M. Leino)
Improved the predictability and robustness of the Dafny program verifier, generating custom triggers to prevent spurious quantifier instantiations and matching loops.
3 months internship in Redmond, WA
华为 | Huawei
Designed and implemented a fast upper body limb detection and tracking engine based on Bayesian inference in graphical models.
6 weeks internship in Shenzhen, China
École Polytechnique (LIX, supervised by Stéphane Graham-Lengrand)
Improved the performance of the Psyche theorem prover by extending its DPLL module to allow restarts.
3 months research project in Palaiseau, France
CSSI Communication & Systèmes
Built a Fortran static analyzer to analyze control flow, build call graphs, and locate dead code.
1 month internship in Le Plessis Robinson, France
Entrepreneurship
Launched YìXué Chinese Dictionary, a paid English-Chinese dictionary for Windows Phone. YìXué sold over 1000 copies, achieved a 4.7★ rating with over 200 reviews, and was featured three times on Microsoft's app store.
Launched and maintained Create Synchronicity, an open source backup & synchronization app (450k downloads, 2k daily users, translated to 30 languages). Featured in PC Magazine's Best free software of 2011 and Computer Bild's Open Source DVD.
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).
Robert B. Guenassia Award, MIT (2015).
Programming Languages Mentoring Workshop travel grant, POPL (2015).
2nd place, École Polytechnique's Best Group Research Project, for research on webcam-based gaze tracking (2013).
2nd place, Microsoft France's App Awards, a mobile development contest, for YìXué Chinese Dictionary (2013).
3rd place, Computer Science competitive entrance exam of the École Normale Supérieure (ENS Ulm) (2011).
4th place, French Olympiads in Mathematics, Paris division (2008).
Community service and mentorship
Co-chairing CAV2021's artifact evaluation committee.
Served in the artifact evaluation committees of POPL'16 and '18, on the program committee of LATTE'21, on the student program committee of IEEE S&P'19, and reviewed for NASA's Formal Methods Symposium, the Journal of Statistical Computation and Simulation, and the Journal of Functional Programming.
Volunteered at PLDI'18 and SPLASH'18.
Mentored six undergraduate and two MS-level MIT students for periods of six to eighteen months, providing guidance and hands-on software design and verification experience (2014-2020).
Held walk-in office hours for early-undergraduate alumni of Association Tremplin, a French non-profit working to encourage high-school students from disadvantaged neighborhoods to pursue a higher education (2012; 4 hours per week for 7 months).
Co-organized the 26th French national session of the European Youth Parliament (2009), authoring grant proposals to raise 20k€, securing sponsorships and in-kind contributions, and hosting 150 participants for a 4-days workshop.
Skills
Software design & development: Wrote professional software in C#, Emacs Lisp, Python, TypeScript, JavaScript, VB.Net, and C++. Other languages include OCaml, Coq, HTML+CSS, C, Java, Dafny, F⋆, Racket, PHP.
Languages: French (mother tongue, French citizen),
English (fluent),
Spanish,
Chinese,
Japanese (basic)
Algorithms & optimization: attended several invitation-only intensive training sessions in algorithms organized by the French branch of the International Olympiads in Informatics.
Randomized algorithms: Implemented randomized algorithms for SAT solving, polynomial equality testing, maximum bipartite matching, string searching, equality testing, logspace counting, and various streaming algorithms.
Information theory: Implemented and optimized a family of low-density parity codes based on MAP estimation in Tanner graphs.
Extra-curricular activities
Blogged about mathematics, programming, and formal verification; got featured in the Code Project's Insider daily newsletter.
Launched a twitter feed about Chinese linguistics and etymology, with over 500 subscribers.
Launched or contributed to many free software projects since 2012, 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 (wrote biblio.el, ESH, company-coq, F⋆-mode, and boogie-friends; co-maintained Flycheck and Proof-General).
All publications
ASPLOSEffective Simulation & Debugging for High-Level Hardware Languages Using Software Compilerspdf, bib
Proceedings of the 26th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2021).
CoqPLAutomated Synthesis of Verified Firewallspdf, bib
The Seventh International Workshop on Coq for PL (CoqPL 2021).
Workshop paper.
CoqPLAn experience report on writing usable DSLs in Coqpdf, bib
The Seventh International Workshop on Coq for PL (CoqPL 2021).
Workshop paper.
SLEUntangling Mechanized Proofspdf, bib
Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering (SLE 2020).
IJCARExtensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofspdf, bib
International Joint Conference on Automated Reasoning (IJCAR 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).
ESOPMeta-F⋆ : Proof Automation with SMT, Tactics, and Metaprogramspdf, bib
Proceedings of the 28th European Symposium on Programming (ESOP 2019).
SETTACorrect-by-Construction Implementation of Runtime Monitors Using Stepwise Refinementpdf, bib
Proceedings of the 4th International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2018).
MLML as a Tactic Language, Againpdf, bib
ML family workshop at ICFP 2018 (ML 2018).
Workshop paper.
SNAPLThe End of History? Using a Proof Assistant to Replace Language Design with Library Designpdf, bib
2nd Summit on Advances in Programming Languages (SNAPL 2017).
CAVTrigger Selection Strategies to Stabilize Program Verifierspdf, bib
Computer Aided Verification: 28th International Conference (CAV 2016).
CoqPLCompany-Coq: Taking Proof General one step closer to a real IDEpdf, bib
The Second International Workshop on Coq for PL (CoqPL 2016).
Workshop paper.
MS thesisCompilation Using Correct-by-Construction Program Synthesishtml, pdf, bib
Master's Thesis at MIT.
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).
Tech reportOutlier Detection in Heterogeneous Datasets using Automatic Tuple Expansionpdf, bib
Technical report.