picture

Clément Pit-Claudel

I'm a senior applied scientist at Amazon AWS, soon to join EPFL as an assistant professor. Previously, I was a PhD candidate at MIT with Adam Chlipala. My research focuses on programming languages, compilers, and formal verification; my broader interests include systems engineering, hardware design languages, security, performance engineering, databases, and type theory.

Prospective students: hi! Check out this dedicated page. I'm starting a new research group at EPFL and I have PhD and post-doc positions open for 2022-2023.

Research

My current research program is organized around three main axes:

My faculty application research summary (pdf) had more info. The following are some concrete recent 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.

Selected publications

2021

ASPLOSEffective Simulation and Debugging for a High-Level Hardware Language 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.

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

AEC Co-chair: CAV 2021

PC member: PLDI'22, LATTE'21, PLOS'21

AEC member: POPL'16, POPL'18

Student PC member: IEEE S&P'19

Journal reviewer: NASA's Formal Methods Symposium, Journal of Statistical Computation and Simulation, Journal of Functional Programming

Conference volunteer: PLDI'18, SPLASH'18

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 and F⋆, and Emacs packages for bibliography management, 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).

Apparently, some of my highest-cited writing is 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.