| 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 | 127 | 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 | 92 | 2020 |
| Trigger selection strategies to stabilize program verifiers KRM Leino, C Pit-Claudel Computer Aided Verification: 28th International Conference, CAV 2016 …, 2016 | 77 | 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 | 58 | 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 | 43 | 2019 |
| Outlier detection in heterogeneous datasets using automatic tuple expansion C Pit-Claudel, Z Mariet, R Harding, S Madden | 38 | 2016 |
| Untangling mechanized proofs C Pit-Claudel Proceedings of the 13th ACM SIGPLAN International Conference on Software …, 2020 | 30 | 2020 |
| 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 | 29 | 2020 |
| The end of history? Using a proof assistant to replace language design with library design A Chlipala, B Delaware, S Duchovni, JS Gross, CF Pit-Claudel, ... Dagstuhl Research, 2017 | 25 | 2017 |
| Company-Coq: Taking Proof General one step closer to a real IDE CF Pit-Claudel, P Courtieu, C Pit-Claudel | 20 | 2016 |
| 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 | 16 | 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 | 13 | 2022 |
| 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 | 8 | 2021 |
| Compilation using correct-by-construction program synthesis C Pit-Claudel Massachusetts Institute of Technology, 2016 | 8 | 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 | 7 | 2018 |
| Linear Matching of JavaScript Regular Expressions A Barrière, C Pit-Claudel Proceedings of the ACM on Programming Languages 8 (PLDI), 1336-1360, 2024 | 5 | 2024 |
| Foundational Integration Verification of a Cryptographic Server A Erbsen, J Philipoom, D Jamner, A Lin, S Gruetter, C Pit-Claudel, ... Proceedings of the ACM on Programming Languages 8 (PLDI), 1704-1729, 2024 | 3 | 2024 |
| A Coq Mechanization of JavaScript Regular Expression Semantics N De Santo, A Barrière, C Pit-Claudel Proceedings of the ACM on Programming Languages 8 (ICFP), 1003-1031, 2024 | 2 | 2024 |
| Relational compilation: Functional-to-imperative code generation for performance-critical applications C Pit-Claudel Massachusetts Institute of Technology, 2022 | 2 | 2022 |
| Incremental Proof Development in Dafny with Module-Based Induction S Ho, C Pit-Claudel arXiv preprint arXiv:2401.16233, 2024 | 1 | 2024 |
Adam ChlipalaMIT CSAILVerified email at csail.mit.edu
