[1] Jason Gross and Andres Erbsen. 10 years of superlinear slowness in Coq, August 2022. Submitted to The Coq Workshop 2022. [ bib | .pdf ]
In most programming languages, asymptotic performance issues can almost always be explained by reference to the algorithm being implemented. At most, the standard asymptotic performance of explicitly used operations on chosen data structures must be considered. Even the constant factors in performance bottlenecks can often be explained without reference to the implementation of the interpreter, compiler, nor underlying machine.

In 10+ years of working with Coq, we (the authors of this proposal and their colleagues) have found this pattern, which holds across multiple programming languages, to be the exception rather than the rule in Coq! This turns performant proof engineering, and especially performant proof automation engineering, from a straightforward science into an arcane form of wizardry.

By presenting in detail a sampling of examples, we propose a defense of the thesis: Performance bottlenecks in proof automation almost always result from inefficiencies in parts of the system which are conceptually distant from the theorem being proven. Said another way, debugging, understanding, and fixing performance bottlenecks in automated proofs almost always requires extensive knowledge of the proof engine, and almost never requires any domain-specific knowledge of the theorem being proven. Further, there is no clear direction of improvement: We know of no systematic proposal, nor even folklore among experts, of what primitives and performance characteristics are sufficient for a performant proof engine.

We hope to start a discussion on the obvious corollary of this thesis: This should not be!

Our presentation, we hope, will serve as a call for a POPLMark for Proof Engines, a call for designing and implementing a proof engine for scalable performant modular proof automation.

[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 file was generated by bibtex2html 1.99.