added abstract to readme. corrected url in paper.

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.