Clément Pit-Claudel

Registered user since Mon 4 Jan 2016

Name:Clément Pit-Claudel
Bio:

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. I work on end-to-end verified compilation pipelines from high-level specifications to assembly language, verified compilers and fast simulation for rule-based hardware design languages with EHRs, and Coq tooling.

Country:United States
Affiliation:MIT / AWS
Research interests:Proof assistants, extensible compilers, programming languages, hardware design languages, optimization, databases, and type theory

Contributions

POPL 2023 Committee Member in Program Committee within the POPL-track
PLDI 2022 Committee Member in PLDI within the PLDI-track
Session Chair of Hardware I (part of PLDI)
Author of Relational Compilation for Performance-Critical Applications within the PLDI-track
Session Chair of Memory (part of PLDI)
CoqPL 2022 Invited Speaker of Coq meets literate programming: tools for documenting, preserving, and sharing mechanized proofs within the CoqPL-track
Invited Speaker in Invited speaker within the CoqPL-track
SPLASH 2021 Author of The Essence of Bluespec: A Core Language for Rule-Based Hardware Design within the SIGPLAN Papers-track
Session Chair of OOPSLA 2020 Papers 4 (part of SIGPLAN Papers)
Author of Untangling mechanized proofs within the SIGPLAN Papers-track
CoqPL 2021 Author of An experience report on writing usable DSLs in Coq within the CoqPL-track
Author of Automated Synthesis of Verified Firewalls within the CoqPL-track
SLE 2020 Author of Untangling Mechanized Proofs within the SLE-track
PLDI 2020 Author of The Essence of Bluespec: A Core Language for Rule-Based Hardware Design within the PLDI Research Papers-track
DeepSpec 2018 Speaker of Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats within the DeepSpec 2018-track
ESOP 2019 Author of Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms within the ESOP 2019-track
ML 2018 Author of ML as a Tactic Language, Again within the ML 2018-track
ICFP 2019 Author of Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats within the Research Papers-track
POPL 2018 Committee Member in Artifact Evaluation Committee within the Artifact Evaluation-track
CoqPL 2016 Author of Company-Coq: Taking Proof General one step closer to a real IDE within the CoqPL-track
POPL 2016 Committee Member in Artifact Evaluation committee within the Artifact Evaluation-track