Clément Pit-Claudel

blogtwitteremailcvpgp 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!



MIT, Cambridge
Research focusing on formal logic, programming languages, and verification

Currently studying towards a PhD in Computer Science, advised by Adam Chlipala. MSc completed in 2016.

2011 – 14

École Polytechnique, Palaiseau
Specialization in computer science

Diplôme d'ingénieur 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.

GPA: 4.35/4.4

2009 – 11

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.



Correct-by-Construction Implementation of Runtime Monitors Using Stepwise Refinement (pdf, bib)

Teng Zhang, John Wiegley, Theophilos Giannakopoulos, Gregory Eakman, Clément Pit-Claudel, Insup Lee, Oleg Sokolsky. Proceedings of the 4th International Symposium Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2018)


The End of History? Using a Proof Assistant to Replace Language Design with Library Design (pdf, bib)

Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye. 2nd Summit on Advances in Programming Languages (SNAPL 2017)


Compilation Using Correct-by-Construction Program Synthesis (web-friendly, pdf, bib)

Clément Pit-Claudel. Master's Thesis at MIT; William A. Martin Memorial Thesis Award for Outstanding Thesis in CS

Trigger Selection Strategies to Stabilize Program Verifiers (pdf, bib)

Rustan Leino, Clément Pit-Claudel. Computer Aided Verification: 28th International Conference (CAV 2016)

Company-Coq: Taking Proof General one step closer to a real IDE (pdf, bib)

Clément Pit-Claudel, Pierre Courtieu. CoqPL'16: The Second International Workshop on Coq for PL


Outlier Detection in Heterogeneous Datasets using Automatic Tuple Expansion (tr)

Clément Pit-Claudel, Zelda Mariet, Rachael Harding, Sam Madden

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant (pdf, bib)

Benjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala. Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015)

Professional experience


Implemented reflective pattern-matching tactics for F*; contributed to research on effect erasure.

(INRIA – 3 months internship in Paris supervised by Cătălin Hriţcu)


Improved the predictability of the Dafny program verifier, generating triggers to prevent spurious quantifier instantiations and matching loops.

(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)

2012 – 13

Volunteered as an English tutor working with École Polytechnique classmates to improve their English.

(École Polytechnique – 6 months teaching assignment)

2011 – 12

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)

Entrepreuneurial initiatives

2013+Launched YìXué Chinese Dictionary, a paid English-Chinese dictionary for Windows Phone. YìXué was featured three times on Microsoft's app store.
2009+Created Create Synchronicity, an open source backup & synchronization app (350k downloads, 2k daily users, translated to 29 languages). Featured in PC Magazine's Best free software of 2011 list and included in Computer Bild's Open Source DVD.

Community service

Served in artifact evaluation committees for POPL'16 and '18, and as external reviewer for NASA's 8th Formal Methods Symposium.

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 hosting 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).

Extra-curricular activities

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); 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

Received a 2017 Frederick C. Hennie III Teaching Award in Recognition of Outstanding Contributions to Departmental Teaching


Languages: French (mother tongue),
English (fluent – TOEFL iBT 119/120),
Chinese (notions),
Japanese (beginner)

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, JavaScript, VB.Net, and C++. Other languages include Java, C, OCaml, Gallina, Dafny, F*, Racket, PHP, HTML/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.