Jason Gross

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