diff --git a/paper/gtt.tex b/paper/gtt.tex
index 549847afce2063f2186ff2f1b751ceec5d2a44d9..2a2d1da72e9b6fc395a73f187d71e5d91087872b 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -408,11 +408,16 @@ However, the dichotomy between gradual and optional typing is not as
 firm as one might like.
 %
 There have been many different proposed semantics of run-time type
-checking: ``transient'' cast semantics only checks the head connective
-of a type (number, function, list, \ldots), ``eager'' cast semantics
-checks run-time type information on closures, whereas ``lazy'' cast
-semantics will always delay a type-check on a function until it is
-called~\cite{vitousekswordssiek:2017,siek+09designspace,findler-felleisen02,hermanXXspaceefficient}.
+checking: ``transient'' cast semantics
+(\cite{vitousekswordssiek:2017}) only checks the head connective of a
+type (number, function, list, \ldots), ``eager'' cast semantics
+(\cite{hermanXXspaceefficient}) checks run-time type information on
+closures, whereas ``lazy'' cast semantics \citep{findler-felleisen02}
+will always delay a type-check on a function until it is
+called.
+%
+See \cite{siek+09designspace} for a presentation of eager and lazy
+semantics, and some points in between.
 %
 The extent to which these different semantics have been shown to
 validate type-based reasoning has been limited to syntactic type