This is a list of projects that I would love to see happen. Alas, lacking infinite time, I don’t have any concrete plans to make them happen, but I’d be happy to advise and mentor others undertaking these projects. Some of these might serve as good bachelor’s or master’s thesis projects, while others are likely too ambitious or not adequately ambitious. I’ve included estimates of how much work I think each project would take me, so adjust accordingly for your greater or lesser experience with the domain. The bottom of the list has some less ambitious projects.

  1. Proving well-typedness of quotation in MetaCoq

    • Context: Löb’s theorem says □(□X → X) → □X where □T means { t : Ast.term & Σ ;;; [] |- t : <% T %> }. The two biggest undertakings in getting such a theorem about a substantial AST are quotation (□X → □□X) and decidable equality of ASTs. MetaCoq largely has decidable equality of ASTs already, and this project is about completing quotation, and in particular the second projection, that the function quote : { t : Ast.term & Σ ;;; [] |- t : T } → Ast.term which adds a layer of quotation gives something that is well-typed, i.e., that we have ∀ v, Σ ;;; [] |- quote v : <% { t : Ast.term & Σ ;;; [] |- t : T } %>.
    • Partial work: JasonGross/metacoq@coq-8.16+quotation-typing, MetaCoq/metacoq/quotation/
    • Estimated commitment: 1–2 major design decisions + 8k–800k loc (defining quote took about 8k loc and 200 hours wakatime)
    • Notes:
      • There are two major blockers at the current state of this project:
        1. Having a version of the safechecker that produces unsquashed typing derivations. I believe Théo Winterhalter may be working on this.

        2. Figuring out how to deal with universes / universe polymorphism of typing judgments. Roughly the problem is: given the definition of quote_prod : (A → Ast.term) → (B → Ast.term) → A × B → Ast.term, how do we formulate the proof that whenever the two arguments always generate well-typed Ast.terms, the result of quote_prod is also well-typed, given that I may use this across different universes. (See also qpair_cps for a slightly simpler version of this problem.)

          Some notes on the current state of systematically handling universes in quoted terms and a likely solution:

          • The problem is that, as far as I can tell, Coq ASTs are not in general quantified over their universe variables, so a systematic treatment must quantify over any template or polymorphic universes at the Gallina level. (Quotation is supposed to be possible in a fixed global environment, so we cannot simply add a polymorphic constant to the global env for every polymorphic definition we wish to quote.) That is, it seems that a quoter for option A should emit not something of type option A -> AST.term, but something of type option A -> Instance.t -> AST.term.
          • To systematically handle these instances, we should treat every quotation as being the quotation of a template/universe polymorphic constant. Any time we quote a constant, inductive, etc, we must thread through the “natural” universe instance, and abstract at the Gallina level over all occurrences of these universes. When we are quoting a term, we should be parametrized on both the natural universe instance of the term we are quoting, and the replacement instance.  
      • The next major issue after these is likely:
        1. Figuring out how to abstract over Gallina context variables so that we can adequately deduplicate work across safechecker invocations (probably we can turn external quantifications into internal ones and safecheck the abstracted term, but some details need to be worked out).
      • And finally if that’s solved, the next two major issues I forsee are:
        1. The axioms used by the various parts of MetaCoq, and whether or not they cause problems when duplicated into the quoted Γ
        2. I’m worry about size of terms and performance a bit, things might be painful.
  2. Löb’s theorem in MetaCoq: For those who think the above project is not ambitious enough. This Agda code might be a good reference for how to build the abstractions.
  3. Denotation in MetaCoq
    • On pain of inconsistency, we cannot write a function denote : { T : Ast.term & { t : Ast.term & Σ ;;; [] |- t : T } → { T : Type & T }. I argue in slides 23–28 and 38 of the presentation of Accelerating Verified-Compiler Development with a Verified Rewriting Engine that it should be possible to paramterize a denotation function over collections in a way that allows effectively having such a denotation function for any subset of the language. The domain of any given instantiation of the denotation function would not, of course, include its own quotation, only those of more restrictive families. MetaCoq’s Template Coq automation could automatically emit specialized instantiations on-the-fly, though, allowing effective use of the denotation function. See this Zulip thread for some more discussion.
    • Estimated commitment: maybe a couple years? Probably PhD-thesis worthy if fully accomplished.
  4. Reflective rewriting based on MetaCoq
  5. Integrating abstract interpretation and reflective rewriting
  6. Removing needless non-zero assumptions from Coq’s ZArith library
    • Many of the lemmas have premises of the form x <> 0 even when the conclusion holds without such premises. Automating goals in Z is much nicer when the relevant lemmas don’t require such assumptions.
    • Existing work: coq/coq#16203 performs this reorganization for N, see also this comment
    • Estimated commitment: the work on N was +765,-270, the work on Z should be 1×–2× as involved
  7. Fill out Coq’s theory of primitive integers.
    • There’s some work in progress on a theory of integers modulo n; I’d love to see this extended/completed and applied to Coq’s Uint63 and Sint63.
    • Additionally, it would be nice to have the basic order modules and relation structure (such as transitivity of comparison) filled out.
    • Finally, zify, lia, and nia don’t work quite as well on int as on Z, N, nat, due to all the moduli. It would be nice to figure out an efficient strategy for deciding linear and nonlinear equations modulo a fixed modulus.
  8. Extending printing reduction effects to timing effects.
    • Estimated commitment: 10–100 loc, probably at most a couple days of work
  9. Extending reduction effects to the VM and native compiler.
  10. Extending rewrite_strat with cbv and lazy reduction ordering strategies (currently it supports only topdown, bottomup, subterms, innermost, outermost).
  11. Establish a methodology for performing PHOAS passes that need to produce both expr-like output and data-like output simultaneously without exponential blowup
    • Concretely:
    • Idea: Currently we’re trying to write a pass that is expr var1 * expr var2 -> A * expr var3. If we define an expr-like-tree-structure that (a) doesn’t use higher-order things for Abs nodes, and (b) stores A at every node, then I think we can write a pass that is expr var1 * expr var2 -> A * tree-of-A and then expr var1 * expr var2 * tree-of-A -> expr var3 such that we incur only linear overhead.
    • Estimated commitment if I were doing it: maybe a day for mit-plv/fiat-crypto#1604 and a couple days to a week for mit-plv/fiat-crypto#1761, and then a couple weeks to a month or two to make the performance charts, write up a clean functional-pearl implementation, and write a conference paper.