picture

Clément Pit-Claudel

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

2014+

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.

2011 – 14

É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.

2009 – 11

Lycée Louis-le-Grand (Paris, France)
Classes préparatoires, MP Info
Specialization in Mathematics and Physics.Served as elected class representative.

Selected publications

2021

ASPLOSEffective Simulation & Debugging for High-Level Hardware Languages Using Software Compilerspdf, bibClément Pit-Claudel, Thomas Bourgeat, Stella Lau, Arvind, Adam Chlipala.
Proceedings of the 26th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2021).

2020

SLEUntangling Mechanized Proofspdf, bibClément Pit-Claudel.
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, bibClément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala.
International Joint Conference on Automated Reasoning (IJCAR 2020).

PLDIThe Essence of Bluespec: A Core Language for Rule-Based Hardware Designpdf, bibThomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, Arvind.
Proceedings of the ACM on Programming Languages (PLDI 2020).

2019

ICFPNarcissus: Correct-by-Construction Derivation of Decoders and Encoders from Binary Formatspdf, bibBenjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala.
Proceedings of the ACM on Programming Languages (ICFP 2019).

2017

SNAPLThe End of History? Using a Proof Assistant to Replace Language Design with Library Designpdf, bibAdam 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).

2016

CAVTrigger Selection Strategies to Stabilize Program Verifierspdf, bibK. Rustan M. Leino and Clément Pit-Claudel.
Computer Aided Verification: 28th International Conference (CAV 2016).

CoqPLCompany-Coq: Taking Proof General one step closer to a real IDEpdf, bibClément Pit-Claudel, Pierre Courtieu.
The Second International Workshop on Coq for PL (CoqPL 2016).
Workshop paper.

2015

POPLFiat: Deductive Synthesis of Abstract Data Types in a Proof Assistantpdf, bibBenjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala.
Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015).

Complete list of publications.

Teaching experience

2016

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

2012 – 13

É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

2011 – 12

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

2017

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

2015

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

2013

华为 | 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

2009

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

2013 – 17

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.

2009+

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, bibClément Pit-Claudel, Thomas Bourgeat, Stella Lau, Arvind, Adam Chlipala.
Proceedings of the 26th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2021).

CoqPLAutomated Synthesis of Verified Firewallspdf, bibShardul Chiplunkar, Clément Pit-Claudel, Adam Chlipala.
The Seventh International Workshop on Coq for PL (CoqPL 2021).
Workshop paper.

CoqPLAn experience report on writing usable DSLs in Coqpdf, bibClément Pit-Claudel, Thomas Bourgeat.
The Seventh International Workshop on Coq for PL (CoqPL 2021).
Workshop paper.

SLEUntangling Mechanized Proofspdf, bibClément Pit-Claudel.
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, bibClément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala.
International Joint Conference on Automated Reasoning (IJCAR 2020).

PLDIThe Essence of Bluespec: A Core Language for Rule-Based Hardware Designpdf, bibThomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, Arvind.
Proceedings of the ACM on Programming Languages (PLDI 2020).

ICFPNarcissus: Correct-by-Construction Derivation of Decoders and Encoders from Binary Formatspdf, bibBenjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala.
Proceedings of the ACM on Programming Languages (ICFP 2019).

ESOPMeta-F⋆ : Proof Automation with SMT, Tactics, and Metaprogramspdf, bibGuido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Cătălin Hriţcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy.
Proceedings of the 28th European Symposium on Programming (ESOP 2019).

SETTACorrect-by-Construction Implementation of Runtime Monitors Using Stepwise Refinementpdf, bibTeng Zhang, John Wiegley, Theophilos Giannakopoulos, Gregory Eakman, Clément Pit-Claudel, Insup Lee, Oleg Sokolsky.
Proceedings of the 4th International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2018).

MLML as a Tactic Language, Againpdf, bibGuido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Cătălin Hriţcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy.
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, bibAdam 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).

CAVTrigger Selection Strategies to Stabilize Program Verifierspdf, bibK. Rustan M. Leino and Clément Pit-Claudel.
Computer Aided Verification: 28th International Conference (CAV 2016).

CoqPLCompany-Coq: Taking Proof General one step closer to a real IDEpdf, bibClément Pit-Claudel, Pierre Courtieu.
The Second International Workshop on Coq for PL (CoqPL 2016).
Workshop paper.

MS thesisCompilation Using Correct-by-Construction Program Synthesishtml, pdf, bibClément Pit-Claudel.
Master's Thesis at MIT.

POPLFiat: Deductive Synthesis of Abstract Data Types in a Proof Assistantpdf, bibBenjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala.
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, bibClément Pit-Claudel, Zelda Mariet, Rachael Harding, Sam Madden.
Technical report.