Clément Pit-Claudel

Registered user since Mon 4 Jan 2016

Name: Clément Pit-Claudel

Bio: I’m a PhD candidate at MIT, working in Adam Chlipala’s lab. My research focuses on proof assistants, extensible compilers, and programming languages; my broader interests include hardware design languages, optimization, 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.
And I’m applying for faculty positions this year!

Country: United States

Affiliation: MIT CSAIL

Personal website: http://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

SLE 2020Author of Untangling Mechanized Proofs within the SLE-track
DeepSpec 2018Speaker of Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats within the DeepSpec 2018-track
ESOP 2019Author of Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms within the ESOP 2019-track
ML 2018Author of ML as a Tactic Language, Again within the ML 2018-track
ICFP 2019Author of Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats within the Research Papers-track
POPL 2018Committee Member in Artifact Evaluation Committee within the Artifact Evaluation-track
CoqPL 2016Author of Company-Coq: Taking Proof General one step closer to a real IDE within the CoqPL-track
POPL 2016Committee Member in Artifact Evaluation committee within the Artifact Evaluation-track