Clément Pit-Claudel
Clément Pit-Claudel
Verified email at - Homepage
Cited by
Cited by
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
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
Trigger selection strategies to stabilize program verifiers
KRM Leino, C Pit-Claudel
Computer Aided Verification: 28th International Conference, CAV 2016 …, 2016
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
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
Outlier detection in heterogeneous datasets using automatic tuple expansion
C Pit-Claudel, Z Mariet, R Harding, S Madden
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
Untangling mechanized proofs
C Pit-Claudel
Proceedings of the 13th ACM SIGPLAN International Conference on Software …, 2020
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
Company-Coq: Taking Proof General one step closer to a real IDE
CF Pit-Claudel, P Courtieu, C Pit-Claudel
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
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
Compilation using correct-by-construction program synthesis
C Pit-Claudel
Massachusetts Institute of Technology, 2016
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
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
Relational compilation: Functional-to-imperative code generation for performance-critical applications
C Pit-Claudel
Massachusetts Institute of Technology, 2022
Diagrammatic notations for interactive theorem proving
S Chiplunkar, C Pit-Claudel
4th International Workshop on Human Aspects of Types and Reasoning Assistants, 2023
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
Incremental Proof Development in Dafny with Module-Based Induction
S Ho, C Pit-Claudel
arXiv preprint arXiv:2401.16233, 2024
Linear Matching of JavaScript Regular Expressions
A Barrière, C Pit-Claudel
arXiv preprint arXiv:2311.17620, 2023
The system can't perform the operation now. Try again later.
Articles 1–20