Publications (20)
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…
A Comparison of Robust Kalman Filters for Improving Wheel-Inertial Odometry in Planetary Rovers
Shounak Das, Cagri Kilic, Ryan Watson +1
This paper compares the performance of adaptive and robust Kalman filter algorithms in improving wheel-inertial odometry on low featured rough terrain. Approaches include classical…
Towards a unified and verified understanding of group-operation networks
Wilson Wu, Louis Jaburi, Jacob Drori +1
A recent line of work in mechanistic interpretability has focused on reverse-engineering the computation performed by neural networks trained on the binary operation of finite grou…
Design of Stickbug: a Six-Armed Precision Pollination Robot
Trevor Smith, Madhav Rijal, Christopher Tatsch +6
This work presents the design of Stickbug, a six-armed, multi-agent, precision pollination robot that combines the accuracy of single-agent systems with swarm parallelization in gr…
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…
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…