| 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 | 170 | 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 | 59 | 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 | 26* | 2023 |
| Relational compilation for performance-critical applications C Pit-Claudel, J Philipoom, D Jamner, A Erbsen, A Chlipala ACM| Proceedings of the 43rd ACM SIGPLAN International Conference on …, 2022 | 16* | 2022 |
| 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 | 15 | 2023 |
| CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version) J Kuepper, A Erbsen, J Gross, O Conoly, C Sun, S Tian, D Wu, A Chlipala, ... arXiv preprint arXiv:2211.10665, 2022 | 15* | 2022 |
| 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 |
| 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 | 6 | 2024 |
| 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 | 6 | 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 |
| Foundational Integration Verification of Diverse Software and Hardware Components A Erbsen Massachusetts Institute of Technology, 2023 | 3 | 2023 |
| Distributed Authorization in Vanadium A Erbsen, A Shankar, A Taly arXiv preprint arXiv:1607.02192, 2016 | 3 | 2016 |
| 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 |
| Modeling High-Level Public-Key Cryptography in Coq A Erbsen | | 2015 |
| A Cryptographically Protected Phone System A Erbsen, A Yedidia | | 2014 |
| CryptOpt: Automatic Optimization of Straightline Code J Kuepper, D Wu, A Erbsen, J Gross, O Conoly, C Sun, S Tian, A Chlipala, ... | | |
Adam ChlipalaMIT CSAILBestätigte E-Mail-Adresse bei csail.mit.edu