diff --git a/trees/dt/dt-001Z.tree b/trees/dt/dt-001Z.tree
--- a/trees/dt/dt-001Z.tree
+++ b/trees/dt/dt-001Z.tree
@@ -3,11 +3,9 @@
 \taxon{Lecture}
 \title{Constructions on [cpos](dt-001D) and PCF}
 \author{liamoc}
-\p{This lecture is based on material from [[haskellhutt]], [[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].}
+\p{This lecture is based on material from [[haskellhutt]], [[jlongley]],[[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].}
 \transclude{dt-002K}
 \transclude{dt-002Z}
 \transclude{dt-0030}
 \transclude{dt-003E}
-\subtree{
-\title{PCF}
-}
+\transclude{dt-003T}
diff --git a/trees/dt/dt-003M.tree b/trees/dt/dt-003M.tree
new file mode 100644
--- /dev/null
+++ b/trees/dt/dt-003M.tree
@@ -0,0 +1,13 @@
+\import{dt-macros}
+\taxon{Definition}
+\author{liamoc}
+\title{The language PCF}
+\p{
+  The language for \strong{P}rogramming \strong{C}omputable \strong{F}unctions (PCF) is a variant of typed #{\lambda}-calculus with minimal extensions to be Turing-complete.
+  ##{
+  \begin{array}{lcl}
+     e & \Coloneqq & n \mid x \mid \lambda x : \tau.\ e \mid e_1\ e_2\mid\mathsf{succ} \mid \mathsf{pred} \mid \mathsf{ifz}\ e_1\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 \mid \mathsf{fix}\ x : \tau.\ e \\
+    \tau & \Coloneqq & \mathsf{nat} \mid \tau_1 \rightarrow \tau_2	 	
+   \end{array}
+  }
+}
\ No newline at end of file
diff --git a/trees/dt/dt-003N.tree b/trees/dt/dt-003N.tree
new file mode 100644
--- /dev/null
+++ b/trees/dt/dt-003N.tree
@@ -0,0 +1,16 @@
+\import{dt-macros}
+\taxon{Definition}
+\author{liamoc}
+\title{Typing rules for [PCF](dt-003M)}
+\p{
+  ##{
+  \inferrule{n \in \mathbb{N}}{\Gamma \vdash n : \mathsf{nat}}\quad
+  \inferrule{x : \tau \in \Gamma}{\Gamma \vdash x : \tau}\quad
+  \inferrule{\Gamma, x : \tau_1 \vdash e : \tau_2  }{ \Gamma \vdash \lambda x : \tau_1.\ e : \tau_1 \rightarrow \tau_2}\quad 
+  \inferrule{\Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2 \quad \Gamma \vdash e_2 : \tau_1}{\Gamma \vdash e_1\ e_2 : \tau_2}\\[2em]
+  \inferrule{ }{ \Gamma \vdash \mathsf{succ} : \mathsf{nat} \rightarrow \mathsf{nat}}\quad 
+  \inferrule{ }{ \Gamma \vdash \mathsf{pred} : \mathsf{nat} \rightarrow \mathsf{nat}}\quad
+  \inferrule{ \Gamma \vdash e_1 : \mathsf{nat} \quad \Gamma \vdash e_2 : \tau \quad \Gamma \vdash e_3 : \tau }{ \Gamma \vdash \mathsf{ifz}\ e_1\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 : \tau}\quad
+  \inferrule{ \Gamma, x : \tau \vdash e : \tau }{\Gamma \vdash \mathsf{fix}\ x : \tau.\ e : \tau}
+  }
+}
\ No newline at end of file
diff --git a/trees/dt/dt-003O.tree b/trees/dt/dt-003O.tree
new file mode 100644
--- /dev/null
+++ b/trees/dt/dt-003O.tree
@@ -0,0 +1,21 @@
+\import{dt-macros}
+\author{liamoc}
+\title{Type-dependent denotations}
+\p{
+Because [PCF](dt-003M) is [typed](dt-003N), we shall assign denotations only to well-typed expressions. 
+The range of our [denotation function](dt-0001) for expressions is determined by the \em{type} of its input expression. That is, the denotation of a type #{\tau} \em{is} the [cpo](dt-001D) whose elements will be the denotations of expressions of type #{\tau}. 
+
+The denotation of the type #{\mathsf{nat}}, then, is merely the [flat domain](dt-0008) of the natural numbers #{\mathbb{N}_\bot}:
+##{
+\llbracket \mathsf{nat} \rrbracket = \mathbb{N}_\bot
+}
+And, the denotation of the function type is the domain of [continuous functions](dt-002F) on cpos:
+##{
+\llbracket \tau_1 \rightarrow \tau_2 \rrbracket = \llbracket \tau_1 \rrbracket \contto \llbracket \tau_2 \rrbracket
+}
+A \em{closed} term #{e : \tau} with no free variables denotes an element of #{\llbracket \tau \rrbracket}, so we might be tempted to define our denotation function for expressions #{e : \tau} like so: ##{\llbracket e \rrbracket : \llbracket \tau \rrbracket}
+However, if #{e : \tau} involves free variables from our context #{\Gamma}, the valuation of #{e} will depend on the values assigned to all the variables. Thus, the denotation of a typed expression #{\Gamma \vdash e : \tau} is defined instead as a [continuous](dt-001J) function:
+##{\llbracket e \rrbracket_\Gamma : \llbracket \Gamma \rrbracket \contto \llbracket \tau \rrbracket}
+where the meaning of a context #{\Gamma = (x_0 : \tau_0, x_1 : \tau_1,\dots, x_n : \tau_n)} will be a a big #{n}-tuple of the values assigned to each variable:
+##{\llbracket \Gamma \rrbracket = \llbracket \tau_0 \rrbracket \times \llbracket \tau_1 \rrbracket \times \cdots \times \llbracket \tau_n \rrbracket}
+}
diff --git a/trees/dt/dt-003P.tree b/trees/dt/dt-003P.tree
new file mode 100644
--- /dev/null
+++ b/trees/dt/dt-003P.tree
@@ -0,0 +1,31 @@
+\import{dt-macros}
+\author{liamoc}
+\taxon{Definition}
+\title{Semantics of [PCF](dt-003M)}
+\subblock{Types}{
+##{
+  \begin{array}{lcl}
+  \llbracket \mathsf{nat} \rrbracket &=& \mathbb{N}_\bot\\  
+  \llbracket \tau_1 \rightarrow \tau_2 \rrbracket &=& \llbracket \tau_1 \rrbracket \contto \llbracket \tau_2 \rrbracket 
+  \end{array}
+}}
+\subblock{Expressions}{
+  For #{\Gamma : e : \tau}, we have #{\llbracket e \rrbracket_\Gamma : \llbracket \tau \rrbracket } defined as follows:
+##{
+\begin{array}{lcl}
+  \llbracket n \rrbracket_\Gamma(\vec{z}) & =&  n\\
+  \llbracket x \rrbracket_\Gamma(\vec{z}) & = & z_j\ \text{where}\ j\ \text{is largest}\ j\ \text{s.t.}\ x = x_j \\
+\llbracket \lambda x : \tau_1.\ e \rrbracket_\Gamma(\vec{z}) & = & (\boldsymbol{\lambda} v \in \llbracket \tau_1 \rrbracket.\ \llbracket e\rrbracket_{\Gamma, x : \tau_1}(\vec{z}, v))\\
+\llbracket e_1\ e_2 \rrbracket_\Gamma(\vec{z}) & = & \llbracket e_1 \rrbracket_\Gamma(\vec{z})(\llbracket e_2 \rrbracket_\Gamma(\vec{z}))\\
+\llbracket \mathsf{succ} \rrbracket_\Gamma(\vec{z}) & = & (\boldsymbol{\lambda} v \in \mathbb{N}_\bot.\ v + 1)\\
+\llbracket \mathsf{pred} \rrbracket_\Gamma(\vec{z}) & = & (\boldsymbol{\lambda} v \in \mathbb{N}_\bot.\ v - 1)\\
+\llbracket \mathsf{ifz}\ e_1\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 \rrbracket_\Gamma(\vec{z}) & = &  \begin{cases}
+    \llbracket e_2 \rrbracket_\Gamma(\vec{z}) & \text{if}\ 		\llbracket e_1 \rrbracket_\Gamma(\vec{z}) > 0 \\
+    \llbracket e_3 \rrbracket_\Gamma(\vec{z}) & \text{if}\ 		\llbracket e_1 \rrbracket_\Gamma(\vec{z}) = 0 \\
+    \bot & \text{if}\ \llbracket e_1 \rrbracket_\Gamma(\vec{z}) = \bot
+  \end{cases}\\
+\llbracket \mathsf{fix}\ x : \tau.\ e \rrbracket_\Gamma(\vec{z}) &= & \mathbf{fix}(\boldsymbol{\lambda} v \in \llbracket \tau \rrbracket.\ \llbracket e\rrbracket_{\Gamma, x : \tau}(\vec{z}, v))
+\end{array}
+}
+In the above definitions a boldface lambda #{\boldsymbol{\lambda}} is used for an anonymous [continuous function](dt-001J) — boldface to distinguish it from the lambda in the [syntax of PCF](dt-003M). Verifying that these functions are indeed [continuous](dt-001J) is straightforward, but is necessary to justify the use of [the #{\mathbf{fix}} operator](dt-001Q). 
+}
diff --git a/trees/dt/dt-003Q.tree b/trees/dt/dt-003Q.tree
new file mode 100644
--- /dev/null
+++ b/trees/dt/dt-003Q.tree
@@ -0,0 +1,8 @@
+\import{dt-macros}
+\author{liamoc}
+\taxon{Definition}
+\title{Notation for #{n}-tuples}
+\p{Given an #{n}-tuple, i.e. elements of the #{n}-ary [product](dm-0005) #{X_0 \times X_1 \times X_2 \times \dots \times X_n}, we typically denote the entire #{n}-tuple as in vector notation: ##{\vec{x} : X_0 \times X_1 \times X_2 \times \dots \times X_n}
+And individual elements of the tuple are accessed with numeric subscripts:
+##{x_0 : X_0 \quad x_2 : X_2 \quad \cdots}
+ }
\ No newline at end of file
diff --git a/trees/dt/dt-003R.tree b/trees/dt/dt-003R.tree
new file mode 100644
--- /dev/null
+++ b/trees/dt/dt-003R.tree
@@ -0,0 +1,25 @@
+\import{dt-macros}
+\author{liamoc}
+\title{Extending [PCF](dt-003M) with product types}
+\p{We shall extend [the syntax of PCF](dt-003M) with a new type former, #{\tau_1 \times \tau_2} and three expression-level constructs for constructing and deconstructing pairs:
+##{
+  \begin{array}{lcl}
+     e & \Coloneqq & \cdots \mid (e_1,e_2) \mid \mathsf{fst}\ e \mid \mathsf{snd}\ e \\
+    \tau & \Coloneqq & \cdots \mid \tau_1 \times \tau_2
+   \end{array}
+}
+Adding to our [typing rules](dt-003N) similarly:
+##{
+  \inferrule{\Gamma \vdash e_1 : \tau_1 \quad e_2 : \tau_2}{(e_1,e_2) : \tau_1 \times \tau_2}\\[2em]
+  \inferrule{\Gamma \vdash e : \tau_1 \times \tau_2}{\Gamma \vdash \mathsf{fst}\ e : \tau_1}\quad
+  \inferrule{\Gamma \vdash e : \tau_1 \times \tau_2}{\Gamma \vdash \mathsf{snd}\ e : \tau_2}
+}
+To extend our [semantics](dt-003P), we make the product type #{\tau_1 \times \tau_2} denote the [product cpo](dt-0021) #{\llbracket \tau_1 \rrbracket \times \llbracket \tau_2 \rrbracket}, and our expression semantics are expressed straightforwardly using our [projection](dt-0020) and [split](dt-0023) operations for [products](dt-002K):
+##{
+  \begin{array}{lcl}
+  \llbracket (e_1, e_2) \rrbracket_\Gamma &=& \langle \llbracket e_1 \rrbracket_\Gamma, \llbracket e_2 \rrbracket_\Gamma \rangle \\
+  \llbracket \mathsf{fst}\ e \rrbracket_\Gamma & = & \pi_0 \circ \llbracket e \rrbracket_\Gamma \\
+  \llbracket \mathsf{snd}\ e \rrbracket_\Gamma & = & \pi_1 \circ \llbracket e \rrbracket_\Gamma \\
+  \end{array}
+}
+}
diff --git a/trees/dt/dt-003S.tree b/trees/dt/dt-003S.tree
new file mode 100644
--- /dev/null
+++ b/trees/dt/dt-003S.tree
@@ -0,0 +1,29 @@
+\import{dt-macros}
+\author{liamoc}
+\title{Extending [PCF](dt-003M) with sum types}
+\p{We shall extend [the syntax of PCF](dt-003M) with a new type former, #{\tau_1 + \tau_2} and three expression-level constructs for constructing and deconstructing sums:
+##{
+  \begin{array}{lcl}
+     e & \Coloneqq & \cdots \mid \mathsf{inl}\ e \mid \mathsf{inr}\ e \mid \mathsf{case}\ e_0\ \mathsf{of}\ \mathsf{inl}\ x \rightarrow e_1 ; \mathsf{inr}\ y \rightarrow e_2 \\
+    \tau & \Coloneqq & \cdots \mid \tau_1 + \tau_2
+   \end{array}
+}
+Adding to our [typing rules](dt-003N) similarly:
+##{
+  \inferrule{\Gamma \vdash e : \tau_1}{\Gamma \vdash \mathsf{inl}\ e : \tau_1 + \tau_2}\quad
+  \inferrule{\Gamma \vdash e : \tau_2}{\Gamma \vdash \mathsf{inr}\ e : \tau_1 + \tau_2}\\[2em]
+  \inferrule{\Gamma \vdash e_0 : \tau_1 + \tau_2 \quad \Gamma, x : \tau_1 \vdash e_1 : \tau \quad \Gamma, y : \tau_2 \vdash e_2 : \tau}{ \Gamma \vdash \mathsf{case}\ e_0\ \mathsf{of}\ \mathsf{inl}\ x \rightarrow e_1 ; \mathsf{inr}\ y \rightarrow e_2 : \tau}
+}
+To extend our [semantics](dt-003P), we make the sum type #{\tau_1 + \tau_2} denote the [sum cpo](dt-0031) #{\llbracket \tau_1 \rrbracket + \llbracket \tau_2 \rrbracket}, and our expression semantics are expressed using our [primitive functions for sums](dt-003D).
+##{
+  \begin{array}{lcl}
+  \llbracket \mathsf{inl}\ e \rrbracket_\Gamma & = & \mathit{inl} \circ \llbracket e \rrbracket_\Gamma \\
+  \llbracket \mathsf{inr}\ e \rrbracket_\Gamma & = & \mathit{inr} \circ \llbracket e \rrbracket_\Gamma
+  \end{array}
+}
+##{
+  \begin{array}{l}\llbracket \mathsf{case}\ e_0\ \mathsf{of}\ \mathsf{inl}\ x \rightarrow e_1 ; \mathsf{inr}\ y \rightarrow e_2  \rrbracket_\Gamma(\vec{z}) \\
+  \quad = 
+  [ \boldsymbol{\lambda}v. \llbracket e_1 \rrbracket_{\Gamma,x:\tau_1}(\vec{z},v), \boldsymbol{\lambda}v. \llbracket e_2 \rrbracket_{\Gamma,y:\tau_2}(\vec{z},v)] (\llbracket e_0 \rrbracket_\Gamma(\vec{z}))\end{array}
+}
+}
diff --git a/trees/dt/dt-003T.tree b/trees/dt/dt-003T.tree
new file mode 100644
--- /dev/null
+++ b/trees/dt/dt-003T.tree
@@ -0,0 +1,10 @@
+\title{PCF}
+\author{liamoc}
+\p{For most purposes in [semantics](dt-0001), describing semantics in terms of ([continuous](dt-001J) functions on) [cpos](dt-001D) is enough. To demonstrate, we will give semantics to PCF: a Turing-complete, higher order functional programming language. We will then extend PCF to include more features, namely pairs (product types) and sum types.}
+\transclude{dt-003M}
+\transclude{dt-003N}
+\transclude{dt-003O}
+\transclude{dt-003Q}
+\transclude{dt-003P}
+\transclude{dt-003R}
+\transclude{dt-003S}
\ No newline at end of file
diff --git a/trees/dt/dt-macros.tree b/trees/dt/dt-macros.tree
--- a/trees/dt/dt-macros.tree
+++ b/trees/dt/dt-macros.tree
@@ -1,10 +1,18 @@
 \def\cal[body]{#{\mathcal{\body}}}
 \def\syn[body]{#{\mathsf{\body}}}
+\def\inferrule[top][bottom]{\dfrac{\top}{\bottom}}
 \def\proofblock[body]{\scope{
 \put\transclude/toc{false}
 \put\transclude/numbered{false}
 \subtree{\taxon{Proof}
 \body
+}}}
+\def\subblock[tile][body]{\scope{
+\put\transclude/toc{false}
+\put\transclude/numbered{false}
+\subtree{
+  \title{\tile}
+  \body
 }}}
 \def\upshotblock[body]{\scope{
 \put\transclude/toc{false}
diff --git a/trees/people/jcb.tree b/trees/people/jcb.tree
--- a/trees/people/jcb.tree
+++ b/trees/people/jcb.tree
@@ -3,4 +3,4 @@
 \meta{external}{https://www.julianbradfield.org/academic.html}
 \meta{institution}{[[uoe]]}
 \meta{position}{Reader}
-\meta{doi}{0000-0002-6223-3489}
+\meta{orcid}{0000-0002-6223-3489}
diff --git a/trees/people/jlongley.tree b/trees/people/jlongley.tree
new file mode 100644
--- /dev/null
+++ b/trees/people/jlongley.tree
@@ -0,0 +1,8 @@
+\title{John Longley}
+\taxon{Person}
+\meta{external}{https://homepages.inf.ed.ac.uk/jrl/}
+\meta{institution}{[[uoe]]}
+\meta{position}{Lecturer}
+
+
+