blog • twitter • email • cv • pgp keys
I'm a grad student at MIT, working in Adam Chlipala's lab to create tools to make software more reliable. My research focuses on proof assistants, compilers, and programming languages, and my broader interests include databases, optimization, type theory, and linguistics. I host free software on SourceForge and GitHub, and I publish apps for Windows Phone and Android. Check out my blog, read my papers, say hi on twitter, or shoot me an email!
Research focusing on formal logic, programming languages, and verification
Currently studying towards a PhD in Computer Science, advised by Adam Chlipala
École Polytechnique, Palaiseau
Specialization in computer science
Diplôme d'ingénieurModules 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
Specialization in mathematics and computer science
Classes préparatoires (MP Info). Modules include Mathematics, Physics and Computer Science. Served as elected class representative.
Master's Thesis at MIT; William A. Martin Memorial Thesis Award for Outstanding Thesis in CS.
Computer Aided Verification: 28th International Conference.
CoqPL'16: The Second International Workshop on Coq for PL.
Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015).
Improved the predictability of the Dafny program verifier, generating triggers to prevent spurious quantifier instantiations and avoid matching loops in the SMT solver.
(Microsoft Research – 3 months internship in Redmond, WA supervised by K. Rustan M. Leino)
Designed and implemented a fast upper body limb detection and tracking framework based on Bayesian inference in graphical models.
(华为 | Huawei – 6 weeks internship in Shenzhen, China)
Improved the performance of the Psyche theorem prover, extending its DPLL module to allow restarts.
(École Polytechnique – 3 months research project supervised by Stéphane Lengrand)
Volunteered as an English tutor working with École Polytechnique classmates to improve their English.
(École Polytechnique – 6 months teaching assignment)
Organized and taught training sessions in mathematics and physics targeted at motivated teenagers from low-income neighborhoods, to increase their chances of getting into college.
(Association Tremplin – 8 months internship in Paris, France)
Built a Fortran static analyzer to analyze control flow, build call graphs, and locate dead code
(CSSI Communication & Systèmes – 1 month internship in Le Plessis Robinson, France)
Member of the artifact evaluation committee of POPL 2016.
Participated in an international session of the European Youth Parliament, drafting bills for review by the European Parliament.
Co-organized the 26th French national session of the European Youth Parliament, raising 20k€ and coordinating the logistics to host 250 persons for 4 days.
Completed a volunteer work program of 80 hours, brushing up trails and glazing windows in the Adirondacks national park (Landmark Volunteers, NY, USA).
Blogged about mathematics and programming, getting 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 various free software projects: wrote plugins and translations for Rockbox (a free audio player firmware) and contributed to multiple Emacs packages (wrote company-coq, F*-mode, and boogie-friends; co-maintained Flycheck and Proof-General)
As president of the Japan student association of the École Polytechnique, established a partnership with the Japan Cultural Institute in Paris (MCJP) granting students free access to exhibitions hosted by the MCJP, co-organized conferences about Japan, launched a film society showing Japanese movies, and co-organized the Japan student association annual alumni dinner
Ranked 4th in the 2008 French Olympiads in Mathematics, Paris division.
Ranked 3rd in the computer science competitive entrance exam of the École Normale Supérieure (ENS Ulm)
Ranked 2nd in Microsoft France's App Awards, a mobile phone application contest, for my YìXué Chinese Dictionary application.
Ranked 2nd in École Polytechnique's Group Research Projects Awards for research on webcam-based gaze tracking.
Received the 2015 Robert B. Guenassia Award at MIT
Received the 2016 William A. Martin Memorial Thesis Award for Outstanding Thesis in CS at MIT
Languages: French (mother tongue),
English (fluent – TOEFL iBT 119/120),
Algorithms & optimization: attended several invitation-only intensive training sessions in algorithms organized by the French branch of the International Olympiads in Informatics.
Software design & development: Developed professional applications in C#, Emacs Lisp, Python, Java, VB.Net, and C++. Other languages include Java, C, OCaml, Gallina, PHP, HTML, and CSS.
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.