Jason Gross

Contact Me

Email: jgross@mit.edu

Office: 32-G822

Code, Résumé, and Curriculum Vitæ

Eventually, my projects will be integrated into this page. In the meantime, please visit my GitHub account, or look at my résumé (general, for computer science, or for mathematics) or curriculum vitæ.

These days, I'm working on 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 ten-hundred most used words (checked by The Up-Goer Five Words Typing-Box): 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.

Papers and Presentations

[1] 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 164-172, 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
[2] 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 h-levels, 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.

[3] Jason Gross. An extensible framework for synthesizing efficient, verified parsers. Master's thesis, Massachusetts Institute of Technology, September 2015. [ bib | .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 low-level details when necessary for performance, and automatic or mostly automatic correctness proofs.

[4] Ben Delaware, Clément Pit-Claudel, Jason Gross, and Adam Chlipala. Fiat: Deductive synthesis of abstract data types in a proof assistant. In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'15), January 2015. [ bib | ACM DL Author-ize Publication | .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 SQL-like query and insert operations. Fiat includes a library for writing specifications of query structures in SQL-inspired 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, correct-by-construction 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 proved-correct rules.

[5] 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/coq-bug-finder.

[6] 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.

[7] 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 code-reasoning throughout the project is now mostly automatic. Although not yet push-button verification (specification-level reasoning, in particular, leaves a lot to be desired) these tactics make a significant step towards that goal. This presentation will cover:
• some programs whose I/O behaviour has been verified (including a simplified version of the echo command-line tool)
• the new automation for fully automatic correctness proofs of Hoare-triple rules for basic instructions
• the new automation for applying Hoare rules for assembly instructions automatically
• the basics of how we're specifying and verifying the I/O behaviour of programs

[8] Jason Gross, Adam Chlipala, and David I. Spivak. Experience implementing a performant category-theory library in Coq. In Proceedings of the 5th International Conference on Interactive Theorem Proving (ITP'14), July 2014. [ bib | arXiv | Springer publication | presentation (.pdf) | presentation (.pptx, annotated with notes) | original conference submission (.pdf) | full bibliography | reviews | .pdf ]
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 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 category-theoretic 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.

[9] Jason Gross. Presentation proposal for of 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.

[10] Jason Gross. Jason Gross' wishlist for Coq, January 2014. [ bib | .pdf ]
[11] Jason Gross. POPL: Minute madness: Category theory in Coq, and program synthesis, January 2014. Presented at the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'14). [ bib | .pdf ]
[12] 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 ]
[13] Jason Gross. Building database management on top of category theory in Coq, January 2013. Presented as a student talk at the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13). [ bib | .pdf ]
[14] 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 SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13). [ bib | .pdf ]
[15] 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 | 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 state-of-the-art 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.97.


[1] Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. Systematic synthesis of elliptic curve cryptography implementations, June 2017. Submitted to PLDI 2017. [ bib | project (GitHub) | artifact (.tar.gz) | .pdf ]
The cryptographic code that runs the Internet is subject to intense manual optimization by elite programmers. Most of the complexity of the optimized code comes from manipulation of integers too large to fit in hardware registers. Perhaps surprisingly, for a change as innocuous as changing an algorithmic parameter to a different prime number, significant pieces of code are rewritten from scratch. Only a handful of experts on the planet are seen as competent enough to do it well, and new implementations (which often include significant amounts of handwritten assembly) tend to take months to code and debug.

In this paper, we demonstrate that the work of those experts can be automated while simultaneously increasing our confidence in code correctness. We implemented a framework in the Coq proof assistant for generating efficient code for elliptic curve cryptography (ECC), with proofs of conformance to a whiteboard-level specification in number theory. While some past projects have verified this kind of code, ours is the first to synthesize it from security parameters. We also have a smaller trusted code base than in past work, as all of our formal reasoning is done within Coq. Still, our generated code is faster than past work that verified clean-slate implementations. We come within a factor of 6 of the running time of the handcrafted world-champion implementations.

[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 (GitHub) | 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 Curry-Howard isomorphism identifies formal proofs with abstract syntax trees of programs; Löb's theorem thus implies, for total languages which validate it, that self-interpreters are impossible. We formalize a few variations of Löb's theorem in Agda using an inductive-inductive 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 context-free 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 Pit-Claudel, Peng Wang, Jason Gross, Ben Delaware, and Adam Chlipala. Correct-by-construction program derivation from specifications to assembly language, June 2015. Submitted to PLDI 2015. [ bib | .pdf ]
We present a Coq-based system to certify the entire process of implementing declarative mathematical specifications with efficient assembly code. That is, we produce formal assembly-code libraries with proofs, in the style of Hoare logic, demonstrating compatibility with relational specifications in higher-order logic. Most code-generation paths from high-level languages involve the introduction of garbage collection and other runtime support for source-level abstractions, but we generate code suitable for resource-constrained embedded systems, using manual memory management and in-place updating of heap-allocated data structures. We start from very high-level source code, applying the Fiat framework to refine set-theory 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 assembly-generation features of the Bedrock framework, where we link with handwritten data-structure implementations and their associated proofs. Each program refinement leads to a proved Hoare-logic 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.97.

Hobbies and Fun Facts

I enjoy wind-surfing, sailing, sky-diving, programming, philosophy, math, physics, learning, and building. I've written up some thoughts on social interactions and emotions, my experience skydiving, and a visual proof that the reals are uncountable, geared at a child. As far as I know, my Erdös Number is 5, because Adam Chlipala's is 4.