From 9f73366440d312925b3287d4153aeb1b7a0c4044 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Tue, 30 Oct 2018 15:00:28 -0400
Subject: [PATCH] spell check
---
paper/gtt.tex | 18 +++++++++---------
1 file changed, 9 insertions(+), 9 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 280d0bd..e4ece66 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -463,7 +463,7 @@ This famously ``fails'' to hold in call-by-value languages in the
presence of effects: if $M$ is a program that prints \texttt{"hello"}
before returning a function, then $M$ will print \emph{now}, whereas
$\lambda x. M x$ will only print when given an argument. But this can be
-accomodated with one further modification: the $\eta$ law is valid in
+accommodated with one further modification: the $\eta$ law is valid in
simple call-by-value languages\footnote{This does not hold in languages
with some intensional feature of functions such as reference
equality. We discuss the applicability of our main results more generally in Section \ref{sec:related}.} (e.g. SML) if we have a ``value
@@ -591,7 +591,7 @@ not change.
%% %
%% We chose call-by-push-value because it follows a similar type
%% theoretic discipline as the negative type lambda calculus: all
-%% connectives internalize some property of the judgmental structure of
+%% connectives internalize some property of the judgemental structure of
%% the system.
%% %
%% Furthermore, since it fully abstractly embeds call-by-value and
@@ -4192,7 +4192,7 @@ We break down this proof into 3 major steps.
language where the casts of GTT are translated to ``contracts'' in
GTT: i.e., CBPV terms that implement the runtime type checking. We
translate the term dynamism of GTT to an inequational theory for CBPV.
- Our translation is parametrized by the implementation of the dynamic
+ Our translation is parameterized by the implementation of the dynamic
types, and we demonstrate two valid implementations, one more direct
and one more Scheme-like.
\item (Section \ref{sec:complex}) Next, we eliminate all uses of complex
@@ -4349,7 +4349,7 @@ However, the interpretation of the dynamic types and the casts between
the dynamic types and ground types $G$ and $\u G$ are not determined
(they were still postulated in Lemma~\ref{lem:casts-admissible}).
%
-For this reason, our translation is \emph{parametrized} by an
+For this reason, our translation is \emph{parameterized} by an
interpretation of the dynamic types and the ground casts.
%
By Theorems~\ref{thm:cast-adjunction}, \ref{thm:retract-general}, we know
@@ -4665,7 +4665,7 @@ assertions provided by upcasts and downcasts.
\caption{Natural Dynamic Type Extension of GTT}
\end{figure}
-The axioms we choose might seem to underspecify the dynamic type, but
+The axioms we choose might seem to under-specify the dynamic type, but
because of the uniqueness of adjoints, the following are derivable.
\begin{lemma}[Natural Dynamic Type Extension Theorems]
The following are derivable in GTT with the natural dynamic type extension
@@ -4783,7 +4783,7 @@ This leads to the following definition:
\[ \texttt{VarArg} = \nu \u Y'. \u Y \with (X \to \u Y') \]
Then we define an open version of $\dynv, \dync$ with respect to a
- variable representing the occurences of $\dynv$ in $\dync$:
+ variable representing the occurrences of $\dynv$ in $\dync$:
\begin{align*}
X \vtype \vdash \dynv_o &= \texttt{Tree}[(1+1) + U \dync_o] \ctype\\
X \vtype \vdash \dync_o &= \texttt{VarArg}[\u F X/\u Y] \ctype\\
@@ -5073,7 +5073,7 @@ in the ep pairs used in Definition~\ref{def:scheme-like-type-interp}.
\subsection{Contract Translation}
-Having defined the data parametrizing the translation, we now consider
+Having defined the data parameterizing the translation, we now consider
the translation of GTT into \cbpvstar\ itself.
%
For the remainder of the paper, we assume that we have a fixed dynamic
@@ -5359,7 +5359,7 @@ rules indexed by type dynamism, but \cbpvstar\ has only \emph{homogeneous}
inequalities between terms, i.e., if $E \ltdyn E'$, then $E,E'$ have
the \emph{same} context and types.
%
-Since every type dynamism judgment has an associated contract, we can
+Since every type dynamism judgement has an associated contract, we can
translate a heterogeneous term dynamism to a homogeneous inequality
\emph{up to contract}. Our next overall goal is to prove
\begin{theorem}[Axiomatic Graduality] \label{thm:axiomatic-graduality}
@@ -8468,7 +8468,7 @@ The (closed) \emph{logical} preorder (for closed values/stacks) is in Figure
\ref{fig:lr}. For every $i$ and value type $A$, we define a relation
$\itylrof \apreorder i A$ between two closed values of type $A$, and for
every $i$ and $\u B$, we define a relation for two ``closed'' stacks $\u
-B \vdash \u F 2$ outputing the observation type $\u F 2$---the
+B \vdash \u F 2$ outputting the observation type $\u F 2$---the
definition is by mutual lexicographic induction on $i$ and $A/\u B$.
Two values or stacks are related if they have the same structure, where
for $\mu,\nu$ we decrement $i$ and succeed if $i = 0$. The shifts $\u
--
GitLab