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:EPFL / AWS

Personal website:https://pit-claudel.fr/clement/

Twitter:https://twitter.com/cpitclaudel

GitHub:https://github.com/cpitclaudel

Research interests:Proof assistants, extensible compilers, programming languages, hardware design languages, optimization, databases, and type theory

Contributions

CoqPL 2023	Committee Member in Program Committee within the CoqPL 2023-track
POPL 2023	Committee Member in Program Committee within the POPL-track
PriSC 2023	Committee Member in Program Committee within the PriSC 2023-track
CPP 2023	Committee Member in Program Committee within the CPP 2023-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
ICFP 2019	Author of Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats within the Research Papers-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
DeepSpec 2018	Speaker of Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats within the DeepSpec 2018-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