@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://jasongross.github.io/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://jasongross.github.io/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://jasongross.github.io/papers/lob-paper/html/lob.html},
url = {https://jasongross.github.io/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://jasongross.github.io/papers/2015-parsing-parse-trees.pdf}
}
@comment{{jabref-meta: databaseType:bibtex;}}
This file was generated by bibtex2html 1.99.