26 citations · 38 across the 9 of their papers we have counts for
9 papers
CryptOpt: Automatic Optimization of Straightline Code
Joel Kuepper, Andres Erbsen, Jason Gross +9
Manual engineering of high-performance implementations typically consumes many resources and requires in-depth knowledge of the hardware. Compilers try to address these problems; h…
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
Jason Gross, Andres Erbsen, Jade Philipoom +2
We address the challenges of scaling verification efforts to match the increasing complexity and size of systems. We propose a research agenda aimed at building a performant proof…
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version)
Joel Kuepper, Andres Erbsen, Jason Gross +9
Most software domains rely on compilers to translate high-level code to multiple different machine languages, with performance not too much worse than what developers would have th…
Accelerating Verified-Compiler Development with a Verified Rewriting Engine
Jason Gross, Andres Erbsen, Jade Philipoom +2
Compilers are a prime target for formal verification, since compiler bugs invalidate higher-level correctness guarantees, but compiler changes may become more labor-intensive to im…
Advantages of maintaining a multi-task project-specific bot: an experience report
Théo Zimmermann, Julien Coolen, Jason Gross +2
Bots are becoming a popular method for automating basic everyday tasks in many software projects. This is true in particular because of the availability of many off-the-shelf task-…
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
Jason Gross, Théo Zimmermann, Rajashree Agrawal +1
As the adoption of proof assistants increases, there is a need for efficiency in identifying, documenting, and fixing compatibility issues that arise from proof assistant evolution…
Extending the team with a project-specific bot
Théo Zimmermann, Julien Coolen, Jason Gross +2
While every other software team is adopting off-the-shelf bots to automate everyday tasks, the Coq team has made a different choice by developing and maintaining a project-specific…
The HoTT Library: A formalization of homotopy type theory in Coq
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine +3
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including un…
Experience Implementing a Performant Category-Theory Library in Coq
Jason Gross, Adam Chlipala, David I. Spivak
We describe our experience implementing a broad category-theory library in Coq. Category theory and computational performance are not usually mentioned in the same breath, but we h…