Jason Gross

According to our database, Jason Gross authored at least 20 papers between 2011 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq.

Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala

J. Autom. Reason., September, 2024

Modular addition without black-boxes: Compressing explanations of MLPs that compute numerical integration.

Chun Hei Yip, Rajashree Agrawal, Lawrence Chan, Jason Gross

CoRR, 2024

Unifying and Verifying Mechanistic Interpretations: A Case Study with Group Operations.

Wilson Wu, Louis Jaburi, Jacob Drori, Jason Gross

CoRR, 2024

Compact Proofs of Model Performance via Mechanistic Interpretability.

Jason Gross, Rajashree Agrawal, Thomas Kwa, Euan Ong, Chun Hei Yip, Alex Gibson, Soufiane Noubir, Lawrence Chan

CoRR, 2024

2023

CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives.

Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom

Proc. ACM Program. Lang., 2023

CryptOpt: Automatic Optimization of Straightline Code.

Joel Kuepper, David Wu, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom

Proceedings of the 45th IEEE/ACM International Conference on Software Engineering: ICSE 2023 Companion Proceedings, 2023

2022

The Advantages of Maintaining a Multitask, Project-Specific Bot: An Experience Report.

Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert

IEEE Softw., 2022

CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives.

Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom

CoRR, 2022

Advantages of maintaining a multi-task project-specific bot: an experience report.

Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert

CoRR, 2022

Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq.

Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Accelerating Verified-Compiler Development with a Verified Rewriting Engine.

Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021

Extending the team with a project-specific bot.

Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert

CoRR, 2021

2020

Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises.

Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala

ACM SIGOPS Oper. Syst. Rev., 2020

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs.

Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2018

Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac.

Jason Gross, Andres Erbsen, Adam Chlipala

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017

The End of History? Using a Proof Assistant to Replace Language Design with Library Design.

Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

The HoTT library: a formalization of homotopy type theory in Coq.

Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2015

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant.

Benjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

2014

Experience Implementing a Performant Category-Theory Library in Coq.

Jason Gross, Adam Chlipala, David I. Spivak

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2011

One shot learning of simple visual concepts.

Brenden M. Lake, Ruslan Salakhutdinov, Jason Gross, Joshua B. Tenenbaum

Proceedings of the 33th Annual Meeting of the Cognitive Science Society, 2011