Follow
Jason Gross
Title
Cited by
Cited by
Year
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
8062011
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
1132015
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
1012020
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
842017
Experience implementing a performant category-theory library in Coq
J Gross, A Chlipala, DI Spivak
International Conference on Interactive Theorem Proving, 275-291, 2014
312014
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
232017
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
International Joint Conference on Automated Reasoning, 119-137, 2020
182020
Reification by parametricity
J Gross, A Erbsen, A Chlipala
International Conference on Interactive Theorem Proving, 289-305, 2018
82018
Systematic generation of fast elliptic curve cryptography implementations
A Erbsen, J Philipoom, J Gross, R Sloan, A Chlipala
Technical Report. https://people. csail. mit. edu/jgross/personal-website …, 2018
72018
The HoTT library
A Bauer, J Gross, PLF Lumsdaine, M Shulman, B Spitters
URL: https://github. com/HoTT/HoTT, 2016
62016
A profiler for Ltac
T Tebbi, J Gross
Coq PL Workshop 2015, 2015
52015
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
32021
Performance Engineering of Proof-Based Software Systems at Scale
JS Gross
Massachusetts Institute of Technology, 2021
32021
An extensible framework for synthesizing efficient, verified parsers
JS Gross
Massachusetts Institute of Technology, 2015
32015
Systematic synthesis of elliptic curve cryptography implementations
A Erbsen, J Philipoom, J Gross, R Sloan, A Chlipala
22016
Coq bug minimizer
J Gross
First International Workshop on Coq for PL (CoqPL’15), 2015
22015
The Speed and Lifetime of Cosmic-Ray Muons
J Gross
MIT, 2011
22011
Advantages of maintaining a multi-task project-specific bot: an experience report
T Zimmermann, J Coolen, J Gross, PM Pédrot, G Gilbert
IEEE Software, 2022
12022
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
J Gross, T Zimmermann, M Poddar-Agrawal, A Chlipala
arXiv preprint arXiv:2202.13823, 2022
12022
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, ...
arXiv preprint arXiv:2211.10665, 2022
2022
The system can't perform the operation now. Try again later.
Articles 1–20