Eventually, my projects will be integrated into this page. In the meantime, please visit my GitHub account, or look at my curriculum vitæ.
These days, I'm working on finishing up my PhD in reflective rewriting, verified cryptographic primitive synthesis, general program synthesis, and category theory on top of homotopy type theory in Coq. I also occasionally commit to the BarnOwl project.
What I do, with only the tenhundred most used words (checked by The UpGoer Five Words TypingBox): It would be nice if we could tell computers what should be done in only a few simple words (but in words that can only mean one thing), and the computers would just know how to do it, and never be slow and never be wrong. I'm working on making this dream come true.
[1] 
Jason S. Gross.
Performance Engineering of ProofBased Software Systems at
Scale.
PhD thesis, Massachusetts Institute of Technology, February 2021.
[ bib 
DSpace@MIT 
presentation (.pdf) 
presentation (YouTube) 
presentation (.pptx) 
.pdf ]
Formal verification is increasingly valuable as our world comes to rely more on software for critical infrastructure. A significant and understudied cost of developing mechanized proofs, especially at scale, is the computer performance of proof generation. This dissertation aims to be a partial guide to identifying and resolving performance bottlenecks in dependently typed tacticdriven proof assistants like Coq. 
[2] 
Jason Gross.
A limited case for reification by type inference, January 2021.
Presented at The
Seventh International Workshop on Coq for Programming Languages (CoqPL'21).
[ bib 
presentation (YouTube) 
code (.v) 
.pdf ]
Proof by reflection is a common and wellstudied automation tool. Reificationgenerally written using L_{tac}, OCaml, typeclasses, or canonical structuresis the means by which a structured representation is derived from an unstructured representation. The reflective automation then operates on the structured representation, relying on an interpretation or denotation function to justify a correspondence between the structured and unstructured representations. 
[3] 
Linden B. Huhmann, Charles F. Harvey, Jason Gross, Anjal Uddin, Imtiaz
Choudhury, Kazi M. Ahmed, John M. Duxbury, Benjamin Bostick, and Alexander
van Geen.
Evaluation of a field kit for testing arsenic in paddy soil
contaminated by irrigation water.
Geoderma, 382:114755, January 2021.
[ bib 
DOI 
publication () ]
Rice is the primary crop in Bangladesh and rice yield is diminished due to the buildup of arsenic (As) in soil from irrigation with highAs groundwater. Soil testing with an inexpensive kit could help farmers target highAs soil for mitigation or decide to switch to a different crop that is less sensitive to As in soil. A total of 3240 field kit measurements of As in 0.5 g of fresh soil added to 50 mL of water were compared with total soil As concentrations measured on ovendried homogenized soil by Xray fluorescence (XRF). For sets of 12 soil samples collected within a series of rice fields, the average of kit As measurements was a linear function of the average of XRF measurements (r^{2} = 0.69). Taking into account that the kit overestimates water As concentrations by about a factor of two, the relationship suggests that about a quarter of the As in paddy soil is released in the kit’s reaction vessel. Using the relationship and considering XRF measurements as the reference, the 12sample average determined correctly whether soil As was above or below a 30 mg/kg threshold in 86% of cases where soil As was above the threshold and in 79% of cases where soil As was below the threshold. We also used a Bayesian approach using 12 kit measurements to estimate the probability that soil As was above a given threshold indicated by XRF measurements. The Bayesian approach is theoretically optimal but was only slightly more accurate than the linear regression. These results show that rice farmers can identify highAs portions of their fields for mitigation using a dozen field kit measurements on fresh soil and base their decisions on this information. Keywords: Field kit, Rice paddy, Irrigation, Arsenic 
[4] 
Clément PitClaudel, Peng Wang, Benjamin Delaware, Jason Gross, and Adam
Chlipala.
Extensible extraction of efficient imperative programs with foreign
functions, manually managed memory, and proofs.
In Nicolas Peltier and Viorica SofronieStokkermans, editors,
Proceedings of the 9th International Joint
Conference on Automated Reasoning (IJCAR'20), pages 119137, Cham, June
2020. Springer International Publishing.
[ bib 
DOI 
publication () 
project () ]
We present an original approach to sound program extraction in a proof assistant, using syntaxdriven automation to derive correctbyconstruction imperative programs from nondeterministic functional source code. Our approach does not require committing to a single inflexible compilation strategy and instead makes it straightforward to create domainspecific code translators. In addition to a small set of core definitions, our framework is a large, userextensible collection of compilation rules each phrased to handle specific language constructs, code patterns, or data manipulations. By mixing and matching these pieces of logic, users can easily tailor extraction to their own domains and programs, getting maximum performance and ensuring correctness of the resulting assembly code. 
[5] 
Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala.
Simple highlevel code for cryptographic arithmetic  with proofs,
without compromises.
In Proceedings of the
40th IEEE Symposium on
Security and Privacy (S&P'19), May 2019.
[ bib 
DOI 

project () 
.pdf ]
We introduce a new approach for implementing cryptographic arithmetic in short highlevel code with machinechecked proofs of functional correctness. We further demonstrate that simple partial evaluation is sufficient to transform into the fastestknown C code, breaking the decadesold pattern that the only fast implementations are those whose instructionlevel steps were written out by hand. 
[6] 
Jason Gross, Andres Erbsen, and Adam Chlipala.
Reification by parametricity: Fast setup for proof by reflection, in
two lines of Ltac.
In Jeremy Avigad and Assia Mahboubi, editors, Proceedings of the
9th International Conference on Interactive
Theorem Proving (ITP'18), pages 289305, Cham, July 2018. Springer
International Publishing.
[ bib 
DOI 
publication () 
presentation (.pdf) 
presentation (.pptx, annotated with notes) 
original conference submission (.pdf) 
artifact () 
artifact (.tar.gz) 
.pdf ]
We present a new strategy for performing reification in Coq. That is, we show how to generate firstclass abstract syntax trees from “native” terms of Coq's logic, suitable as inputs to verified compilers or procedures in the proofbyreflection style. Our new strategy, based on simple generalization of subterms as variables, is straightforward, short, and fast. In its pure form, it is only complete for constants and function applications, but “let” binders, eliminators, lambdas, and quantifiers can be accommodated through lightweight coding conventions or preprocessing. 
[7] 
Jason Gross.
Presentation proposal for teaching your rooster to crow in C, July
2018.
Presented at The Coq
Workshop 2018.
[ bib 
code (.html) 
code (.v) 
.pdf ]
Coq's notation system is both extremely powerful and confusingly adhoc. While powerful enough to prettyprint abstract syntax trees in most domainspecific languages, how to do so does not seem to be common knowledge. Typical questions arising from such an endeavor might include “How do I pick notation levels?”, “Why are these notations clashing?”, “Which things should be marked as symbols?”, “How do I use boxes in format?”, and “How do I get parentheses to show up (only) where I want them to?” This interactive presentation aims to serve as a guide to these questions and more, by demonstrating and explaining how to prettyprint subsets of C using only Coq's Notation mechanism. 
[8] 
Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément
PitClaudel, Sorawit Suriyakarn, Peng Wang, and Katherine Ye.
The end of history? using a proof assistant to replace language
design with library design.
In Benjamin S. Lerner, Rastislav Bodík, and Shriram
Krishnamurthi, editors, Proceedings of the
The 2nd Summit oN Advances in Programming
Languages (SNAPL'17), volume 71 of Leibniz International Proceedings
in Informatics (LIPIcs), pages 3:13:15, Dagstuhl, Germany, May 2017.
Schloss DagstuhlLeibnizZentrum fuer Informatik.
[ bib 
DOI 
project homepage 
presentation (.odp) 
presentation (.pdf) 
.pdf ]
Functionality of software systems has exploded in part because of advances in programminglanguage support for packaging reusable functionality as libraries. Developers benefit from the uniformity that comes of exposing many interfaces in the same language, as opposed to stringing together hodgepodges of commandline tools. Domainspecific languages may be viewed as an evolution of the power of reusable interfaces, when those interfaces become so flexible as to deserve to be called programming languages. However, common approaches to domainspecific languages give up many of the hardwon advantages of librarybuilding in a rich common language, and even the traditional approach poses significant challenges in learning new APIs. We suggest that instead of continuing to develop new domainspecific languages, our community should embrace librarybased ecosystems within very expressive languages that mix programming and theorem proving. Our prototype framework Fiat, a library for the Coq proof assistant, turns languages into easily comprehensible libraries via the key idea of modularizing functionality and performance away from each other, the former via macros that desugar into higherorder logic and the latter via optimization scripts that derive efficient code from logical programs. Keywords: domainspecific languages, synthesis, verification, proof assistants, software development 
[9] 
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu
Sozeau, and Bas Spitters.
The HoTT library: A formalization of homotopy type theory in Coq.
In Proceedings of the 6th ACM
SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages
164172, New York, NY, USA, January 2017. ACM.
[ bib 
DOI 
arXiv 

.pdf ]
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 univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types. Keywords: Coq, Higher inductive types, Homotopy type theory, Univalent foundations, Universe polymorphism 
[10] 
Jason Gross.
The HoTT/HoTT library in Coq: Designing for speed, July 2016.
Presented at The 5th International
Congress on Mathematical Software (ICMS 2016).
[ bib 
presentation (.pptx, annotated with notes) 
.pdf ]
The HoTT/HoTT library is one of the major Coq libraries exploring univalent foundations and homotopy type theory, the other being UniMath. The library includes formalization of the basic type formers, some axiomatic higher inductive types including the circle, the interval, suspensions, and quotients, a formalization of modalities (reflective subtoposes) using modules as a way to quantify over all universe levels, formalizations of Cantor spaces and the surreals, the basic theory of hlevels, and a significant amount of category theory centered around comma categories and functoriality of various constructions involving comma categories. A significant amount of work has gone into ensuring that the library compiles quickly. This talk will discuss the various constructions in the HoTT library, as well as the design choices and features, both of Coq and of univalent type theory, which allow our library to compile and typecheck quickly. 
[11] 
Jason Gross.
An extensible framework for synthesizing efficient, verified parsers.
Master's thesis, Massachusetts Institute of Technology, September
2015.
[ bib 
DSpace@MIT 
.pdf ]
Parsers have a long history in computer science. This thesis proposes a novel approach to synthesizing efficient, verified parsers by refinement, and presents a demonstration of this approach in the Fiat framework by synthesizing a parser for arithmetic expressions. The benefits of this framework may include more flexibility in the parsers that can be described, more control over the lowlevel details when necessary for performance, and automatic or mostly automatic correctness proofs. 
[12] 
Tobias Tebbi and Jason Gross.
A profiler for Ltac, January 2015.
Presented at The
First International Workshop on Coq for PL (CoqPL'15).
[ bib 
.pdf ]
We present a simple profiler for the Ltac tactic language of the Coq Proof Assistent. It measures the time spent in invocations of primitive tactics as well as tactics defined in Ltac and their inner invocations. The profiler is controlled using Vernacular commands and prints an aggregated view that differentiates between tactic invocations depending on their call tree location. 
[13] 
Jason Gross.
Coq bug minimizer, January 2015.
Presented at The
First International Workshop on Coq for PL (CoqPL'15).
[ bib 
reviews 
.pdf ]
Are bugs the bane of your existence? Do you dread Coq upgrades, because they mean you'll have to spend days tracking down subtle failures deep in your developments? Have you ever hit an anomaly that just wouldn't go away, and wished you understood what triggered it? Have you ever been tormented by two blocks of code that looked identical, but behaved differently? Do you wish you submit more helpful error reports, but don't want to put in the time to construct minimal examples? If you answered “yes” to any of these questions, then the Coq Bug Minimizer is for you! Clone your own copy at https://github.com/JasonGross/coqbugfinder. 
[14] 
Ben Delaware, Clément PitClaudel, Jason Gross, and Adam Chlipala.
Fiat: Deductive synthesis of abstract data types in a proof
assistant.
In Proceedings of the 42nd
ACM SIGPLANSIGACT Symposium on Principles of Programming Languages
(POPL'15), January 2015.
[ bib 
DOI 

project homepage 
artifact (.tar.gz) 
.pdf ]
We present Fiat, a library for the Coq proof assistant supporting refinement of declarative specifications into efficient functional programs with a high degree of automation. Each refinement process leaves a proof trail, checkable by the normal Coq kernel, justifying its soundness. We focus on the synthesis of abstract data types that package methods with private data. We demonstrate the utility of our framework by applying it to the synthesis of query structures  abstract data types with SQLlike query and insert operations. Fiat includes a library for writing specifications of query structures in SQLinspired notation, expressing operations over relations (tables) in terms of mathematical sets. This library includes a set of tactics for automating the refinement of these specifications into efficient, correctbyconstruction OCaml code. Using these tactics, a programmer can generate such an implementation completely automatically by only specifying the equivalent of SQL indexes, data structures capturing useful views of the abstract data. We conclude by speculating on the new programming modularity possibilities enabled by an automated refinement system with provedcorrect rules. 
[15] 
Jason Gross.
Presentation: Input, output, and automation in x86 proved, August
2014.
Presented at Microsoft Research, Cambridge, UK.
[ bib 
.pptx 
.pdf ]
The x86proved project can now verify assembly programs with input and output! The codereasoning throughout the project is now mostly automatic. Although not yet pushbutton verification (specificationlevel reasoning, in particular, leaves a lot to be desired) these tactics make a significant step towards that goal. This presentation will cover: 
[16] 
Jason Gross, Adam Chlipala, and David I. Spivak.
Experience implementing a performant categorytheory library in
Coq.
In Gerwin Klein and Ruben Gamboa, editors, Proceedings of the
5th International Conference on
Interactive Theorem Proving (ITP'14), pages 275291, Cham, July 2014.
Springer International Publishing.
[ bib 
DOI 
arXiv 
publication () 
presentation (.pdf) 
presentation (.pptx, annotated with notes) 
original conference submission (.pdf) 
full bibliography 
reviews 
.pdf ]
We describe our experience implementing a broad categorytheory library in Coq. Category theory and computational performance are not usually mentioned in the same breath, but we have needed substantial engineering effort to teach Coq to cope with large categorical constructions without slowing proof script processing unacceptably. In this paper, we share the lessons we have learned about how to represent very abstract mathematical objects and arguments in Coq and how future proof assistants might be designed to better support such reasoning. One particular encoding trick to which we draw attention allows categorytheoretic arguments involving duality to be internalized in Coq's logic with definitional equality. Ours may be the largest Coq development to date that uses the relatively new Coq version developed by homotopy type theorists, and we reflect on which new features were especially helpful. 
[17] 
Jason Gross.
Presentation proposal for three neat tricks in Coq 8.5, April 2014.
Presented at the
6th Coq
Workshop.
[ bib 
code (.html) 
code (.v) 
reviews 
.pdf ]
Coq 8.5 has a number of new features. It has more powerful universe polymorphism support. It allows tactics to be run at interpretation to construct other terms. The ability to switch from Gallina to Ltac in arbitrary locations nicely complements the constr: notation permitting the switch from Ltac to Gallina in tactics, and opens up many new possibilities. I propose to present three tricks involving these new features: tactics in terms allows the construction of tactics that recurse under binders; tactics in terms together with typeclasses allows overloading notations based on the type of their arguments; and there is a way to talk about universe levels explicitly, helped along by tactics in terms. 
[18]  Jason Gross. POPL: Minute madness: Category theory in Coq, and program synthesis, January 2014. Presented at the 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL'14). [ bib  .pdf ] 
[19]  Jason Gross. Jason Gross' wishlist for Coq, January 2014. [ bib  .pdf ] 
[20]  Jason Gross. CSAIL student workshop 2013: Computational higher inductive types: Computing with custom equalities, October 2013. Presented at the 2014 MIT CSAIL Student Workshop. [ bib  .pdf ] 
[21]  Jason Gross. POPL: Minute madness: Database management on top of category theory in Coq: Category of relational schemas = category of categories, January 2013. Presented at the 40th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL'13). [ bib  .pdf ] 
[22]  Jason Gross. Building database management on top of category theory in Coq, January 2013. Presented as a student talk at the 40th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL'13). [ bib  .pdf ] 
[23] 
Brenden M. Lake, Ruslan Salakhutdinov, Jason Gross, and Joshua B. Tenenbaum.
One shot learning of simple visual concepts.
In Proceedings of the
33rd
Annual Conference of the Cognitive Science Society, 2011.
[ bib 
project homepage 
videos 
.pdf ]
People can learn visual concepts from just one example, but it remains a mystery how this is accomplished. Many authors have proposed that transferred knowledge from more familiar concepts is a route to one shot learning, but what is the form of this abstract knowledge? One hypothesis is that the sharing of parts is core to one shot learning, and we evaluate this idea in the domain of handwritten characters, using a massive new dataset. These simple visual concepts have a rich internal part structure, yet they are particularly tractable for computational models. We introduce a generative model of how characters are composed from strokes, where knowledge from previous characters helps to infer the latent strokes in novel characters. The stroke model outperforms a competing stateoftheart character model on a challenging one shot learning task, and it provides a good fit to human perceptual data. 
This reference list was generated by bibtex2html 1.99.</p>
[1] 
Jason Gross, Andres Erbsen, Rajashree Agrawal, Jade Philipoom, and Adam
Chlipala.
Accelerating verifiedcompiler development with a verified rewriting
engine, January 2022.
Submitted to POPL 2022.
[ bib 
project () 
artifact (.tar.gz) 
.pdf ]
Compilers are a prime target for formal verification, since compiler bugs invalidate higherlevel correctness guarantees, but compiler changes may become more laborintensive to implement, if they must come with proof patches. One appealing approach is to present compilers as sets of algebraic rewrite rules, which a generic engine can apply efficiently. Now each rewrite rule can be proved separately, with no need to revisit past proofs for other parts of the compiler. We present the first realization of this idea, in the form of a framework for the Coq proof assistant. Our new Coq command takes normal proved theorems and combines them automatically into fast compilers with proofs. We applied our framework to improve the Fiat Cryptography toolchain for generating cryptographic arithmetic, producing an extracted commandline compiler that is about 1000× faster while actually featuring simpler compilerspecific proofs. 
[2] 
Jason Gross, Jack Gallagher, and Benya Fallenstein.
Löb's theorem: A functional pearl of dependently typed quining,
March 2016.
Submitted to ICFP
2016.
[ bib 
project () 
artifact (.zip) 
code (.agda) 
code (.html) 
bibliography 
.pdf ]
Löb's theorem states that to prove that a proposition is provable, it is sufficient to prove the proposition under the assumption that it is provable. The CurryHoward isomorphism identifies formal proofs with abstract syntax trees of programs; Löb's theorem thus implies, for total languages which validate it, that selfinterpreters are impossible. We formalize a few variations of Löb's theorem in Agda using an inductiveinductive encoding of terms indexed over types. We verify the consistency of our formalizations relative to Agda by giving them semantics via interpretation functions. 
[3] 
Jason Gross and Adam Chlipala.
Parsing parses: A pearl of (dependently typed) programming and proof,
August 2015.
Submitted to ICFP
2015.
[ bib 
.pdf ]
We present a functional parser for arbitrary contextfree grammars, together with soundness and completeness proofs, all inside Coq. By exposing the parser in the right way with parametric polymorphism and dependent types, we are able to use the parser to prove its own soundness, and, with a little help from relational parametricity, prove its own completeness, too. Of particular interest is one strange instantiation of the type and value parameters: by parsing parse trees instead of strings, we convince the parser to generate its own completeness proof. We conclude with highlights of our experiences iterating through several versions of the Coq development, and some general lessons about dependently typed programming. 
[4] 
Clément PitClaudel, Peng Wang, Jason Gross, Ben Delaware, and Adam Chlipala.
Correctbyconstruction program derivation from specifications to
assembly language, June 2015.
Submitted to PLDI 2015.
[ bib 
.pdf ]
We present a Coqbased system to certify the entire process of implementing declarative mathematical specifications with efficient assembly code. That is, we produce formal assemblycode libraries with proofs, in the style of Hoare logic, demonstrating compatibility with relational specifications in higherorder logic. Most codegeneration paths from highlevel languages involve the introduction of garbage collection and other runtime support for sourcelevel abstractions, but we generate code suitable for resourceconstrained embedded systems, using manual memory management and inplace updating of heapallocated data structures. We start from very highlevel source code, applying the Fiat framework to refine settheory expressions into functional programs; then we further apply Fiat's refinement tools to translate functional programs into Facade, a simple imperative language without a heap or aliasing; and finally we plug into the assemblygeneration features of the Bedrock framework, where we link with handwritten datastructure implementations and their associated proofs. Each program refinement leads to a proved Hoarelogic specification for an assembly function, with no trust dependencies on any aspect of our synthesis process, which is highly automated. 
This reference list was generated by bibtex2html 1.99.</p>