# jason-gross-drafts.bib

@misc{lob-paper,
author = {Jason Gross and Jack Gallagher and Benya Fallenstein},
title = {L{\"o}b's Theorem: A functional pearl of dependently typed quining},
month = {March},
year = {2016},
note = {Submitted to \href{http://conf.researchr.org/home/icfp-2016/}{ICFP 2016}},
bibliography = {https://people.csail.mit.edu/jgross/personal-website/papers/lob-bibliography.html},
abstract = {L{\"o}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{\"o}b's theorem thus implies, for
total languages which validate it, that self-interpreters are
impossible.  We formalize a few variations of L{\"o}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.},
artifact-zip = {https://people.csail.mit.edu/jgross/personal-website/papers/lob-paper/supplemental-nonymous.zip},
code-agda = {https://people.csail.mit.edu/jgross/personal-website/papers/lob-paper/lob.lagda},
code-github = {https://github.com/JasonGross/lob-paper},
code-html = {https://people.csail.mit.edu/jgross/personal-website/papers/lob-paper/html/lob.html},
url = {https://people.csail.mit.edu/jgross/personal-website/papers/2016-lob-icfp-2016-draft.pdf}
}

@misc{parsing-parse-trees,
author = {Jason Gross and Adam Chlipala},
title = {Parsing Parses: A Pearl of (Dependently Typed) Programming and Proof},
month = {August},
year = {2015},
note = {Submitted to \href{http://icfpconference.org/icfp2015/cfp.html}{ICFP
2015}},
abstract = {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 \emph{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.},
owner = {Jason},
timestamp = {2015.03.14},
url = {https://people.csail.mit.edu/jgross/personal-website/papers/2015-parsing-parse-trees.pdf}
}

@misc{pldi-15-fiat-to-facade,
author = {Cl\'ement Pit--Claudel and Peng Wang and Jason Gross and Ben Delaware
title = {Correct-by-Construction Program Derivation from Specifications to
Assembly Language},
month = {June},
year = {2015},
note = {Submitted to PLDI 2015},
abstract = {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.},
owner = {Jason},
timestamp = {2014.11.17},
}

@misc{pldi-18-fiat-crypto,
author = {Andres Erbsen and Jade Philipoom and Jason Gross and Robert Sloan and Adam Chlipala},
title = {Systematic Generation of Fast Elliptic Curve Cryptography Implementations},
month = {June},
year = {2018},
note = {Submitted to \href{http://pldi18.sigplan.org/home}{PLDI 2018}},
abstract = {Widely used implementations of cryptographic
primitives employ number-theoretic optimizations
specific to large prime numbers used as moduli of
arithmetic.  These optimizations have been applied
manually by a handful of experts, using informal
rules of thumb.  We present the first automatic
compiler that applies these optimizations, starting
from straightforward modular-arithmetic-based
algorithms and producing code around 5X faster than
with off-the-shelf arbitrary-precision integer
libraries for C.  Furthermore, our compiler is
implemented in the Coq proof assistant; it produces
not just C-level code but also proofs of functional
correctness.  We evaluate the compiler on several
key primitives from elliptic curve cryptography.},
artifact-tar-gz = {https://people.csail.mit.edu/jgross/personal-website/papers/2018-fiat-crypto-pldi-anonymous.tar.gz},
code-github = {https://github.com/mit-plv/fiat-crypto},
url = {https://people.csail.mit.edu/jgross/personal-website/papers/2018-fiat-crypto-pldi-draft.pdf}
}

@misc{reification-by-parametricity,
author = {Jason Gross and Andres Erbsen and Adam Chlipala},
title = {Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of {L}tac},
month = {July},
year = {2018},
note = {Submitted to \href{https://itp2018.inria.fr/}{ITP 2018}},
abstract = {We present a new strategy for performing reification in Coq.
That is, we show how to generate first-class abstract syntax trees from native'' terms of Coq's logic, suitable as inputs to verified proof procedures in the \emph{proof by reflection} style.
Our new strategy, based on the \texttt{pattern} tactic, is simple, short, and fast.
We survey the existing methods of reification, describing various design choices and tricks that can be used to speed them up, as well as various limitations.
Our strategy is not a good fit, for example, when a term must be reified without performing $\beta\iota\zeta$ reduction.
We describe the results of benchmarking 18 variants of reification, in addition to our own, finding that our own reification outperforms 16 of these methods in all cases, and one additional method in some cases; the fastest method of reification we tested is writing an OCaml plugin.
Our method is the most concise of the strategies we considered, requiring only two to four lines of \textsc{Ltac}---beyond lists of the identifiers to reify and their reified variants---to reify a term.
Additionally, our strategy automatically provides error messages which are no less helpful than Coq's own error messages.},
artifact-tar-gz = {https://people.csail.mit.edu/jgross/personal-website/papers/2018-reification-by-parametricity-itp-draft.tar.gz},
url = {https://people.csail.mit.edu/jgross/personal-website/papers/2018-reification-by-parametricity-itp-draft.pdf}
}


This file was generated by bibtex2html 1.97.