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
9942011
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
1332020
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
1242015
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
982017
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
362014
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
262020
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
242017
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
102018
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
82018
Performance engineering of proof-based software systems at scale
JS Gross
Massachusetts Institute of Technology, 2021
72021
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
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
42023
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
42021
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
32022
An extensible framework for synthesizing efficient, verified parsers
JS Gross
Massachusetts Institute of Technology, 2015
32015
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 abs/2211.10665, 2022
22022
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
22021
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 system can't perform the operation now. Try again later.
Articles 1–20