Follow
Clément Pit-Claudel
Clément Pit-Claudel
Verified email at epfl.ch - Homepage
Title
Cited by
Cited by
Year
Fiat: Deductive synthesis of abstract data types in a proof assistant
B Delaware, C Pit-Claudel, J Gross, A Chlipala
Acm Sigplan Notices 50 (1), 689-700, 2015
1242015
The essence of Bluespec: a core language for rule-based hardware design
T Bourgeat, C Pit-Claudel, A Chlipala, Arvind
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language …, 2020
732020
Trigger selection strategies to stabilize program verifiers
KRM Leino, C Pit-Claudel
Computer Aided Verification: 28th International Conference, CAV 2016 …, 2016
632016
Meta-F: Proof Automation with SMT, Tactics, and Metaprograms
G Martínez, D Ahman, V Dumitrescu, N Giannarakis, C Hawblitzel, ...
European Symposium on Programming, 30-59, 2019
492019
Narcissus: correct-by-construction derivation of decoders and encoders from binary formats
B Delaware, S Suriyakarn, C Pit-Claudel, Q Ye, A Chlipala
Proceedings of the ACM on Programming Languages 3 (ICFP), 1-29, 2019
38*2019
Outlier detection in heterogeneous datasets using automatic tuple expansion
C Pit-Claudel, Z Mariet, R Harding, S Madden
322016
Untangling mechanized proofs
C Pit-Claudel
Proceedings of the 13th ACM SIGPLAN International Conference on Software …, 2020
282020
Extensible extraction of efficient imperative programs with foreign functions, manually managed memory, and proofs
C Pit-Claudel, P Wang, B Delaware, J Gross, A Chlipala
Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris …, 2020
262020
The end of history? Using a proof assistant to replace language design with library design
A Chlipala, B Delaware, S Duchovni, J Gross, C Pit-Claudel, S Suriyakarn, ...
2nd Summit on Advances in Programming Languages (SNAPL 2017), 2017
242017
Company-Coq: Taking Proof General one step closer to a real IDE
CF Pit-Claudel, P Courtieu, C Pit-Claudel
202016
Effective simulation and debugging for a high-level hardware language using software compilers
C Pit-Claudel, T Bourgeat, S Lau, Arvind, A Chlipala
Proceedings of the 26th ACM International Conference on Architectural …, 2021
132021
Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code
C Pit-Claudel, J Philipoom, D Jamner, A Erbsen, A Chlipala
Proceedings of the 43rd ACM SIGPLAN International Conference on Programming …, 2022
82022
Compilation using correct-by-construction program synthesis
C Pit-Claudel
Massachusetts Institute of Technology, 2016
82016
Correct-by-construction implementation of runtime monitors using stepwise refinement
T Zhang, J Wiegley, T Giannakopoulos, G Eakman, C Pit-Claudel, I Lee, ...
International Symposium on Dependable Software Engineering: Theories, Tools …, 2018
72018
An experience report on writing usable DSLs in Coq
C Pit-Claudel, T Bourgeat
CoqPL’21: The Seventh International Workshop on Coq for PL, 2021
62021
Diagrammatic notations for interactive theorem proving
S Chiplunkar, C Pit-Claudel
4th International Workshop on Human Aspects of Types and Reasoning Assistants, 2023
12023
Hydras & Co.: Formalized mathematics in Coq for inspiration and entertainment
P Castéran, J Damour, K Palmskog, C Pit-Claudel, T Zimmermann
Journées Francophones des Langages Applicatifs: JFLA 2022, 2022
12022
Relational compilation: Functional-to-imperative code generation for performance-critical applications
C Pit-Claudel
Massachusetts Institute of Technology, 2022
12022
A Coq Mechanization of JavaScript Regular Expression Semantics
N De Santo, A Barrière, C Pit-Claudel
arXiv preprint arXiv:2403.11919, 2024
2024
Incremental Proof Development in Dafny with Module-Based Induction
S Ho, C Pit-Claudel
arXiv preprint arXiv:2401.16233, 2024
2024
The system can't perform the operation now. Try again later.
Articles 1–20