diff --git a/papers/scp/PLFA.bib b/papers/scp/PLFA.bib
index 8be50145..3a0b7d79 100644
--- a/papers/scp/PLFA.bib
+++ b/papers/scp/PLFA.bib
@@ -283,4 +283,94 @@
   pages={38--94},
   year={1994},
   publisher={San Diego: Academic Press, c1987-}
-}
\ No newline at end of file
+}
+
+
+@article{Abadi-1991,
+	Author = {Abadi, M. and Cardelli, L. and Curien, P.-L. and Levy, J.-J.},
+	Journal = {Journal of Functional Programming},
+	Number = {4},
+	Pages = {375-416},
+	Title = {Explicit Substitutions},
+	Volume = {1},
+	Year = {1991}}
+
+
+@book{Barendregt-1984,
+	Author = {H.P. Barendregt},
+	Publisher = {Elsevier},
+	Series = {Studies in Logic},
+	Title = {The Lambda Calculus},
+	Volume = {103},
+	Year = {1984}}
+
+
+@inproceedings{Schafer-Tebbi-Smolka-2015,
+	Author = {Steven Sch{\"{a}}fer and Tobias Tebbi and Gert Smolka},
+	Booktitle = {Interactive Theorem Proving - 6th International Conference},
+	Month = {August},
+	Pages = {359--374},
+	Publisher = {Springer},
+	Series = {ITP},
+	Title = {Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions},
+	Year = {2015}}
+
+
+@techreport{Pfenning-1992,
+	Address = {Pittsburgh, PA, USA},
+	Author = {Pfenning, Frank},
+	Institution = {Carnegie Mellon University},
+	Number = {CMU-CS-92-186},
+	Title = {A Proof of the Church-Rosser Theorem and Its Representation in a Logical Framework},
+	Year = {1992}}
+
+
+@article{Siek-2017,
+	Author = {Jeremy G. Siek},
+	Journal = {CoRR},
+	Number = {4},
+	Title = {Revisiting Elementary Denotational Semantics},
+	Volume = {abs/1707.03762},
+	Year = {2017}}
+
+
+@article{Scott-1976,
+	Author = {Dana Scott},
+	Journal = {SIAM Journal on Computing},
+	Number = {3},
+	Pages = {522-587},
+	Title = {Data Types as Lattices},
+	Volume = {5},
+	Year = {1976}}
+
+
+@article{Engeler-1981,
+	Author = {Engeler, Erwin},
+	Journal = {algebra universalis},
+	Month = {Dec},
+	Number = {1},
+	Pages = {389--392},
+	Title = {Algebras and combinators},
+	Volume = {13},
+	Year = {1981}}
+
+
+@article{Plotkin-1993,
+	Author = {Gordon D. Plotkin},
+	Journal = {Theoretical Computer Science},
+	Number = {1},
+	Pages = {351 - 409},
+	Title = {Set-theoretical and other elementary models of the λ-calculus},
+	Volume = {121},
+	Year = {1993}}
+
+
+@article{Barendregt-1983,
+	Author = {Henk Barendregt and Mario Coppo and Mariangiola Dezani-Ciancaglini},
+	Journal = {Journal of Symbolic Logic},
+	Month = {12},
+	Number = {4},
+	Pages = {931-940},
+	Title = {A filter lambda model and the completeness of type assignment},
+	Volume = {48},
+	Year = {1983}}
diff --git a/papers/scp/PLFA.tex b/papers/scp/PLFA.tex
index 669dc2cd..8a0714cf 100755
--- a/papers/scp/PLFA.tex
+++ b/papers/scp/PLFA.tex
@@ -18,7 +18,7 @@
 
 \author[adr1]{Wen Kokke}
 \ead{wen.kokke@ed.ac.uk}
-\author[adr2]{Jeremy Siek}
+\author[adr2]{Jeremy G. Siek}
 \ead{jsiek@indiana.edu}
 \author[adr1]{Philip Wadler\corref{cor1}}
 \ead{wadler@inf.ed.ac.uk}
@@ -287,6 +287,49 @@ with full normalisation (including reduction under lambda terms).  Emphasis
 is put on the correspondence between the structure of a term and
 evidence that it is in normal form.
 
+\paragraph{Substitution: in the untyped lambda calculus}
+Delves deeper into the properties of simultaneous substitution,
+establishing the equations of the $\sigma$ algebra of
+\citet{Abadi-1991}. These equations enable a straightforward proof of
+the Substitution Lemma~\citep{Barendregt-1984}, which is needed in the
+next chapter.
+
+\paragraph{Confluence: of the untyped lambda calculus}
+Presents a proof of the Church-Rosser theorem based on the classic
+idea of parallel reduction due to Tait and Martin-L\"of. The proof in
+Agda is streamlined by the use of ideas from
+\citet{Schafer-Tebbi-Smolka-2015} and \citet{Pfenning-1992}.
+
+\paragraph{Big-step: evaluation for call-by-name}
+Introduces the notion of big-step evaluation to develop a
+deterministic call-by-name reduction strategy. The main result of this
+chapter is a proof that big-step evaluation implies the existence of a
+reduction sequence that terminates with a lambda abstraction.
+
+\subsection*{Part III, Denotational Semantics}
+
+\paragraph{Denotational: semantics of the untyped lambda calculus}
+The early denotational semantics of the lambda calculus based on graph
+models~\citep{Scott-1976,Engeler-1981,Plotkin-1993} and filter
+models~\citep{Barendregt-1983} were particularly simple and elegant.
+This chapter presents such a semantics in a big-step style that is
+approachable to readers familiar with operational semantics.
+
+\paragraph{Compositional: the denotational semantics is compositional}
+TODO
+
+\paragraph{Soundness: of reduction with respect to denotational semantics}
+TODO
+
+\paragraph{Adequacy: of denotational semantics with respect to reduction}
+TODO
+
+
+\paragraph{Contextual Equivalence: is implied by denotational equality}
+TODO
+
+
+
 \subsection*{Discussion}
 
 PLFA and SF differ in several particulars.  PLFA begins with a computationally