| Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises A Erbsen, J Philipoom, J Gross, R Sloan, A Chlipala ACM SIGOPS Operating Systems Review 54 (1), 23-30, 2020 | 159 | 2020 |
| Integration Verification Across Software and Hardware for a Simple Embedded System A Erbsen, S Gruetter, J Choi, C Wood, A Chlipala 42nd ACM SIGPLAN Conference on Programming Language Design and …, 2021 | 56 | 2021 |
| Flexible Instruction-Set Semantics via Type Classes T Bourgeat, I Clester, A Erbsen, S Gruetter, P Singh, A Wright, A Chlipala arXiv preprint arXiv:2104.00762, 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 43rd ACM SIGPLAN Conference on Programming Language Design and …, 2022 | 13 | 2022 |
| CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives J Kuepper, A Erbsen, J Gross, O Conoly, C Sun, S Tian, D Wu, A Chlipala, ... 44th ACM SIGPLAN Conference on Programming Language Design and …, 2023 | 12* | 2023 |
| Omnisemantics: Smooth Handling of Nondeterminism A Charguéraud, A Chlipala, A Erbsen, S Gruetter ACM Transactions on Programming Languages and Systems 45 (1), 1-43, 2023 | 11 | 2023 |
| Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises A Erbsen, J Philipoom, J Gross, R Sloan, A Chlipala 2019 IEEE Symposium on Security and Privacy (SP) 1, 1202-1219, 2019 | 11* | 2019 |
| Reification by parametricity: Fast setup for proof by reflection, in two lines of Ltac J Gross, A Erbsen, A Chlipala Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as …, 2018 | 10 | 2018 |
| Crafting certified elliptic curve cryptography implementations in Coq A Erbsen Massachusetts Institute of Technology, 2017 | 10 | 2017 |
| Integration Verification Across Software and Hardware for a Simple Embedded System. PLDI’21 (2021) A Erbsen, S Gruetter, J Choi, C Wood, A Chlipala | 8 | 2021 |
| Flexible Instruction-Set Semantics via Abstract Monads (Experience Report) T Bourgeat, I Clester, A Erbsen, S Gruetter, P Singh, A Wright, A Chlipala Proceedings of the ACM on Programming Languages 7 (ICFP), 108-124, 2023 | 7 | 2023 |
| Accelerating Verified-Compiler Development with a Verified Rewriting Engine J Gross, A Erbsen, J Philipoom, M Poddar-Agrawal, A Chlipala arXiv preprint arXiv:2205.00862, 2022 | 5 | 2022 |
| Certifying derivation of state machines from coroutines M Ikebuchi, A Erbsen, A Chlipala 49th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages …, 2022 | 5 | 2022 |
| Distributed Authorization in Vanadium A Erbsen, A Shankar, A Taly arXiv preprint arXiv:1607.02192, 2016 | 3 | 2016 |
| Foundational Integration Verification of Diverse Software and Hardware Components A Erbsen Massachusetts Institute of Technology, 2023 | 2 | 2023 |
| Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq J Gross, A Erbsen, J Philipoom, R Agrawal, A Chlipala arXiv preprint arXiv:2305.02521, 2023 | | 2023 |
| Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises A Erbsen, J Philipoom, J Gross, R Sloan, A Chlipala ACM SIGOPS Operating Systems Review 54 (1), 23-30, 2020 | | 2020 |
| Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises A Erbsen, J Philipoom, J Gross, R Sloan, A Chlipala ACM SIGOPS Operating Systems Review 54 (1), 23-30, 2020 | | 2020 |
| Modeling High-Level Public-Key Cryptography in Coq A Erbsen | | 2015 |
| A Cryptographically Protected Phone System A Erbsen, A Yedidia | | 2014 |
Adam ChlipalaMIT CSAILVerified email at csail.mit.edu
