Add title page and missing reference to Takahashi

README.md

@@ -5,18 +5,22 @@ We give Coq formalizations of two proofs showing well-known results
 about the untyped lambda calculus.
 
 The main results are complete proofs of the Postponement and
-Standardization theorems, formalizing
+Standardization theorems, formalizing parts of, respectively:
 
-* ..., and
-* Ryo Kashima. <cite>[A Proof of the Standardization Theorem in
-Lambda-Calculus][kashima]</cite><br>
-  Research Reports on Mathematical and Computing Sciences, C-145, (Tokyo Institute of Technology, 2000).
+* Masako Takahashi.
+  <cite>[Parallel Reductions in Lambda-calculus][takahashi]</cite><br>
+  (Information and Computation, Volume 118, 1995)
+* Ryo Kashima.<cite>[A Proof of the Standardization Theorem in
+  Lambda-Calculus][kashima]</cite><br>
+  Research Reports on Mathematical and Computing Sciences, C-145, (Tokyo
+  Institute of Technology, 2000).
 
 This work was done as a study project by Ignas Vyšniauskas ([@yfyf]) and
 Johannes Emerich ([@knuton]).
 
 [![Lambda Giraffe](https://f.cloud.github.com/assets/47458/1644002/24fac234-58d9-11e3-96b4-4106ce8a9971.png)](http://knuton.github.io/la-girafe-sportive/)
 
 [kashima]: http://www.is.titech.ac.jp/~kashima/pub/C-145.pdf
+[takahashi]: http://dx.doi.org/10.1016/S0747-7171(89)80045-8
 [@yfyf]: https://github.com/yfyf
 [@knuton]: https://github.com/knuton

doc/report.tex

@@ -1,3 +1,4 @@
+%%%% verbatim standard Coq headers with --utf8
 \documentclass[12pt]{report}
 \usepackage[utf8x]{inputenc}
 
@@ -11,8 +12,58 @@
 \usepackage{fullpage}
 \usepackage{coqdoc}
 \usepackage{amsmath,amssymb}
+%%%% END Coq headers
+
+\title{Coq formalisation of \\
+    Postponement and Standardization theorems\\
+    in the untyped lambda-calculus}
+\author{
+    Johannes Emerich
+        \href{mailto:[email protected]}{
+        \normalsize \texttt{([email protected])}}\\
+    Ignas Vyšniauskas
+        \href{mailto:[email protected]}{
+        \normalsize \texttt{([email protected])}}\\
+\\
+  ILLC \\
+  Universiteit van Amsterdam
+  \\
+  \\
+  \emph{under the supervision of}\\
+  \\
+    Dimitri Hendriks
+        \href{mailto:[email protected]}{
+        \normalsize \texttt{([email protected])}}\\
+    Femke van Raamsdonk
+        \href{mailto:[email protected]}{
+        \normalsize \texttt{([email protected])}}\\
+\\
+  Vrije Universiteit Amsterdam
+}
+
+\date{\today}
+
 \begin{document}
 
+\maketitle
+\begin{abstract}
+We give Coq formalizations of two proofs showing well-known results
+about the untyped lambda calculus.
+
+The main results are complete proofs of the Postponement and
+Standardization theorems, formalizing parts of, respectively:
+\begin{itemize}
+    \item Masako Takahashi. ``Parallel Reductions in Lambda-calculus''
+
+    (Information and Computation, Volume 118, 1995)
+    \item Ryo Kashima. ``A Proof of the Standardization Theorem in
+        Lambda-Calculus''
+
+      Research Reports on Mathematical and Computing Sciences, C-145, (Tokyo
+      Institute of Technology, 2000)
+\end{itemize}
+\end{abstract}
+
 \tableofcontents
 
 \input{Untyped}