Merge branch 'master' of https://github.ccs.neu.edu/coqatoos/cbv-gradual-type-theory

paper/gtt.tex

@@ -227,7 +227,7 @@
 \newcommand{\obcast}[2]{\langle{#1}\Leftarrow{#2}\rangle}
 \newcommand{\err}{\mho}
 \newcommand{\diverge}{\Omega}
-\newcommand{\print}{\kw{print}\,\,}
+\newcommand{\print}{\kw{print}}
 \newcommand{\roll}{\kw{roll}}
 \newcommand{\rollty}[1]{\texttt{roll}_{#1}\,\,}
 \newcommand{\unroll}{\kw{unroll}}
@@ -1071,7 +1071,7 @@ computation type of potentially effectful programs that return a value
 of type $A$, while $U \u B$ is the value type of thunked computations of
 type $\u B$.  The introduction rule for $\u F A$ is returning a value of
 type $A$ (\ret{V}), while the elimination rule is sequencing a
-computation of an $\u F A$ with a computation $x : A \vdash M : \u B$ to
+computation $M : \u F A$ with a computation $x : A \vdash N : \u B$ to
 produce a computation of a $\u B$ ($\bindXtoYinZ{M}{x}{N}$).  While any
 closed complex value $V$ is equivalent to an actual value, a computation
 of type $\u F A$ might perform effects (e.g. printing) before returning
@@ -1273,8 +1273,8 @@ types will arise from type dynamism and casts.
 The \emph{type dynamism} relation of gradual type
 theory~\cite{nl18cbngtt} corresponds to the type precision relation of
 \cite{siek} and the na\"ive subtyping of \cite{wadler-findler}.  We
-write type dynamism as $A \ltdyn A'$, which is read as ``$A'$ is more
-dynamic than $A$''; intuitively, this means that $A'$ supports more
+write type dynamism as $A \ltdyn A'$, which is read as ``$A$ is less
+dynamic than $A'$''; intuitively, this means that $A'$ supports more
 behaviors than $A$.  \cite{nl18cbngtt,icfp} analyze this as the
 existence of an \emph{upcast} from $A$ to $A'$ and a downcast from $A'$
 to $A$ which form an embedding-projection pair (\emph{ep pair}) for an