diff --git a/README.md b/README.md
index 9846656..5368dbe 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,21 @@
-lfinlf
-======
+This repository comprises the public LFinLF development, including
+soundness and completeness of translation to canonical forms, family-level
+lambdas, and constants.
+
+The paper draft documenting the proof structure is lfinlf.pdf.
+
+All code by Chris Martens, 2008 - present.
+
+Paper abstract:
+
+We present a mechanized proof of the metatheory of LF, i.e. the decidability of
+typechecking and the existence and uniqueness of canonical forms. We use a
+syntactic approach in which we define a translation from LF to its canonical
+forms presentation (in which only beta-short, eta-long terms are well-formed)
+and prove soundness and completeness of the translation, establishing that
+definitional equivalence in LF corresponds to syntactic equivalence in
+canonical forms. Much recent work is based on the system of canonical
+forms and hereditary substitution presented herein; our proof also serves
+to reconcile that presentation with the traditional version based on
+definitional equivalence.
 
-Mechanized metatheory of LF in Twelf.
\ No newline at end of file
diff --git a/lfinlf.pdf b/lfinlf.pdf
index 4f075fc..a2d3244 100644
Binary files a/lfinlf.pdf and b/lfinlf.pdf differ