Jason Gross

Publication Activity (10 Years)

Years Active: 2011-2024
Publications (10 Years): 22

Top Topics

Presburger Arithmetic

Imperative Programs

Top Venues

Proc. ACM Program. Lang.

IEEE Symposium on Security and Privacy

Publications

Jason Gross, Rajashree Agrawal, Thomas Kwa, Euan Ong, Chun Hei Yip, Alex Gibson, Soufiane Noubir, Lawrence Chan
Compact Proofs of Model Performance via Mechanistic Interpretability. CoRR (2024)
Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. J. Autom. Reason. 68 (3) (2024)
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Joel Kuepper, David Wu, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
CryptOpt: Automatic Optimization of Straightline Code. ICSE Companion (2023)
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
CryptOpt: Automatic Optimization of Straightline Code. CoRR (2023)
Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. CoRR (2023)
Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert
The Advantages of Maintaining a Multitask, Project-Specific Bot: An Experience Report. IEEE Softw. 39 (5) (2022)
Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala
Accelerating Verified-Compiler Development with a Verified Rewriting Engine. CoRR (2022)
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives. CoRR (2022)
Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert
Advantages of maintaining a multi-task project-specific bot: an experience report. CoRR (2022)
Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. ITP (2022)
Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala
Accelerating Verified-Compiler Development with a Verified Rewriting Engine. ITP (2022)
Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. CoRR (2022)
Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert
Extending the team with a project-specific bot. CoRR (2021)
Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. IJCAR (2) (2020)
Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala
Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises. ACM SIGOPS Oper. Syst. Rev. 54 (1) (2020)
Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala
Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. IEEE Symposium on Security and Privacy (2019)
Jason Gross, Andres Erbsen, Adam Chlipala
Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac. ITP (2018)
Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye
The End of History? Using a Proof Assistant to Replace Language Design with Library Design. SNAPL (2017)
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters
The HoTT library: a formalization of homotopy type theory in Coq. CPP (2017)
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters
The HoTT Library: A formalization of homotopy type theory in Coq. CoRR (2016)
Benjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. POPL (2015)
Jason Gross, Adam Chlipala, David I. Spivak
Experience Implementing a Performant Category-Theory Library in Coq. CoRR (2014)
Jason Gross, Adam Chlipala, David I. Spivak
Experience Implementing a Performant Category-Theory Library in Coq. ITP (2014)
Brenden M. Lake, Ruslan Salakhutdinov, Jason Gross, Joshua B. Tenenbaum
One shot learning of simple visual concepts. CogSci (2011)