section 3, 4 edits

paper/gtt.tex

@@ -2725,8 +2725,7 @@ Dually, we have
 \end{longonly}
 
 Together, the universal property for casts and the $\eta$ principles for
-each type imply that the casts must behave like their contract
-implementations:
+each type imply that the casts must behave as in lazy cast semantics:
 \begin{theorem}[Cast Unique Implementation Theorem for $+,\times,\to,\with$] \label{thm:functorial-casts}
 The casts' behavior is uniquely determined as follows: \ifshort (See the extended version for $+$, $\with$.) \fi
 \begin{small}
@@ -4029,8 +4028,8 @@ built-in casts of the gradual language into ordinary terms implemented
 in a non-gradual language.
 %
 While contracts are typically implemented in a dynamically typed
-language, our target is typed, meaning we retain type information
-that might be used in later stages of compilation.
+language, our target is typed, retaining type information similarly to
+manifest contracts \cite{greenberg-manifest}.
 
 Writing $\sem{M}$ for the contract translation, the remaining sections
 of the paper establish:
@@ -4120,10 +4119,10 @@ To implement the casts and dynamic types, we \emph{add} general
 B$, the fixed point of $\u Y \ctype \vdash \u B \ctype$).
 %
 The recursive type $\mu X.A$ is a value type with constructor
-$\kw{roll}$, whose eliminator is pattern matching, whereas the
+$\texttt{roll}$, whose eliminator is pattern matching, whereas the
 corecursive type $\nu \u Y.\u B$ is a computation type defined by its
-eliminator (\kw{unroll}), with an introduction form that we also write
-as \kw{roll}.
+eliminator (\texttt{unroll}), with an introduction form that we also write
+as \texttt{roll}.
 %
 We extend the inequational theory with monotonicity of each term constructor of
 the recursive types, and with their $\beta\eta$ rules.
@@ -4458,7 +4457,7 @@ interpretations:
 
 This dynamic type interpretation is a natural fit for CBPV because the
 introduction forms for $\dynv$ are exactly the introduction forms for
-all of the value types (unit, pairing,$\inl$, $\inr$, $\force$), while
+all of the value types (unit, pairing,$\texttt{inl}$, $\texttt{inr}$, $\texttt{force}$), while
 elimination forms are all of the elimination forms for computation types
 ($\pi$, $\pi'$, application and binding); such ``bityped'' languages
 are related to \cite{girard01locussolum,zeilberger09thesis}.
@@ -4668,8 +4667,8 @@ This leads to the following definition:
   called with any number of dynamically typed value arguments $\dynv$
   and returns a dynamically typed result $\u F \dynv$.  To see why a
   $\dync$ can be called with any number of arguments, observe that its
-  infinite unrolling is $\u F \dynv \with (\dynv \to \u F \dync) \with
-  (\dynv \to \dynv \to \u F \dync) \with \ldots$.  This type is
+  infinite unrolling is $\u F \dynv \with (\dynv \to \u F \dynv) \with
+  (\dynv \to \dynv \to \u F \dynv) \with \ldots$.  This type is
   isomorphic to a function that takes a list of $\dynv$ as input ($(\mu
   X. 1 + (\dynv \times X)) \to \u F \dynv$), but operationally $\dync$
   is a more faithful model of Scheme implementations, because all of the
@@ -4746,8 +4745,8 @@ form for $\dync$.
 The elimination form for $\dynv$ is a typed version of Scheme's
 \emph{match} macro.
 %
-The introduction form for $\dync$ is very similar to a
-typed version of Scheme's \emph{case-lambda} construct.
+The introduction form for $\dync$ is a typed, CBPV version of Scheme's
+\emph{case-lambda} construct.
 %
 Finally, we add type dynamism rules expressing the representations of
 $1$, $A + A$, and $A \times A$ in terms of booleans that were explicit
@@ -5269,8 +5268,8 @@ the left-hand theorem would require more thunks/forces.
   only place where we need to reason about their definitions
   explicitly---afterwards, we can simply use the fact that they are ep
   pairs with the ``pure'' value upcasts and stack downcasts, which
-  compose much more nicely than effectful terms.  The reason is two
-  additional lemmas we prove, which show that a projection is determined
+  compose much more nicely than effectful terms.  This is justified by two
+  additional lemmas, which show that a projection is determined
   by its embedding and vice versa, and that embedding-projections
   satisfy an adjunction/Galois connection property.  The final lemmas
   show that, according to Figure~\ref{fig:cast-to-contract},
@@ -9452,7 +9451,7 @@ In the dual, we don't think of the computation dynamic type as a
 computation types.
 %
 Thinking of the type as unfolding:
-\[ \dync = \u F\dync \wedge (\dynv \to \u F \dync) \wedge (\dynv \to \dynv \to \u F \dync) \wedge \cdots \]
+\[ \dync = \u F\dync \wedge (\dynv \to \u F \dynv) \wedge (\dynv \to \dynv \to \u F \dynv) \wedge \cdots \]
 %
 This says that a dynamically typed computation is one that can be
 invoked with any finite number of arguments on the stack, a fairly

paper/max.bib

@@ -1185,3 +1185,9 @@ pages="36--54",
   number = 3,
   pages = {297--347},
 }
+@inproceedings{greenberg-manifest,
+ author = {Greenberg, Michael and Pierce, Benjamin C. and Weirich, Stephanie},
+ title = {Contracts Made Manifest},
+ series = {POPL '10},
+ year = 2010
+}
\ No newline at end of file