| One shot learning of simple visual concepts B Lake, R Salakhutdinov, J Gross, J Tenenbaum Proceedings of the annual meeting of the cognitive science society 33 (33), 2011 | 1030 | 2011 |
| 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 | 155 | 2020 |
| 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 | 124 | 2015 |
| The HoTT library: a formalization of homotopy type theory in Coq A Bauer, J Gross, PLF Lumsdaine, M Shulman, M Sozeau, B Spitters Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017 | 100 | 2017 |
| Experience implementing a performant category-theory library in Coq J Gross, A Chlipala, DI Spivak Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as …, 2014 | 38 | 2014 |
| 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 | 24 | 2017 |
| 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 |
| CryptOpt: Verified compilation with randomized program search for cryptographic primitives J Kuepper, A Erbsen, J Gross, O Conoly, C Sun, S Tian, D Wu, A Chlipala, ... Proceedings of the ACM on Programming Languages 7 (PLDI), 1268-1292, 2023 | 9* | 2023 |
| Performance engineering of proof-based software systems at scale JS Gross Massachusetts Institute of Technology, 2021 | 8 | 2021 |
| The HoTT library A Bauer, J Gross, PLF Lumsdaine, M Shulman, B Spitters URL: https://github. com/HoTT/HoTT, 2016 | 6 | 2016 |
| Evaluation of a field kit for testing arsenic in paddy soil contaminated by irrigation water LB Huhmann, CF Harvey, J Gross, A Uddin, I Choudhury, KM Ahmed, ... Geoderma 382, 114755, 2021 | 4 | 2021 |
| A profiler for Ltac T Tebbi, J Gross Coq PL Workshop 2015, 2015 | 4 | 2015 |
| 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 | 3 | 2022 |
| An extensible framework for synthesizing efficient, verified parsers JS Gross Massachusetts Institute of Technology, 2015 | 3 | 2015 |
| Extending the team with a project-specific bot T Zimmermann, J Coolen, J Gross, PM Pédrot, G Gilbert arXiv preprint arXiv:2112.07365, 2021 | 2 | 2021 |
| Coq bug minimizer J Gross First International Workshop on Coq for PL (CoqPL’15), 2015 | 2 | 2015 |
| The Speed and Lifetime of Cosmic-Ray Muons J Gross MIT, 2011 | 2 | 2011 |
| 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 | 1 | 2022 |
| The Advantages of Maintaining a Multitask, Project-Specific Bot: An Experience Report T Zimmermann, J Coolen, J Gross, PM Pédrot, G Gilbert IEEE Software 39 (5), 32-37, 2022 | 1 | 2022 |
Adam ChlipalaMIT CSAIL在 csail.mit.edu 的电子邮件经过验证
