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
	and Adam Chlipala},
  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},
  url = {https://people.csail.mit.edu/jgross/personal-website/papers/2015-fiat-to-facade.pdf}
}
@misc{pldi-17-fiat-crypto,
  author = {Andres Erbsen and Jade Philipoom and Jason Gross and Robert Sloan and Adam Chlipala},
  title = {Systematic Synthesis of Elliptic Curve Cryptography Implementations},
  month = {June},
  year = {2017},
  note = {Submitted to \href{http://pldi17.sigplan.org/home}{PLDI 2017}},
  abstract = {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 \emph{verified} this kind of code, ours is
    the first to \emph{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 \emph{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.},
  artifact-tar-gz = {https://people.csail.mit.edu/jgross/personal-website/papers/2017-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/2017-fiat-crypto-pldi-draft.pdf}
}

This file was generated by bibtex2html 1.97.