cites and edits

paper/gtt.tex

@@ -2347,12 +2347,12 @@ $\upcast{A}{\dynv}{x} \equidyn \upcast{A'}{\dynv}{\upcast{A}{A'}{x}}$.
  \dncast{T}{T'}{\upcast{T}{T'}{x}}$ (upcast then downcast might error
  less but but otherwise does not change the behavior) and
  $\upcast{T}{T'}{\dncast{T}{T'}{x}} \ltdyn x$ (downcast then upcast
- might error more but otherwise does not change the behavio).  However,
+ might error more but otherwise does not change the behavior).  However,
  since a value type precision $A \ltdyn A'$ induces a value upcast $x :
  A \vdash \upcast{A}{A'}{x} : A'$ but a stack downcast $\bullet : \u F
  A' \vdash \dncast{\u F A}{\u F A'}{\bullet} : \u F A$ (and dually for
- computations), the statement of the theorem involves the functoriality
- of $U$ and $\u F$ types.
+ computations), the statement of the theorem wraps one cast with 
+ the constructors for $U$ and $\u F$ types (functoriality of $\u F/U$).
 \begin{theorem}[Casts are a Galois Connection] \label{thm:cast-adjunction} ~~~
   \begin{enumerate}
   \item $\bullet' : \u F A' \vdash \bindXtoYinZ{\dncast{\u F A}{\u F A'}{\bullet'}}{x}{\ret{(\upcast{A}{A'}{x})}} \ltdyn \bullet' : \u F A'$
@@ -2774,7 +2774,7 @@ The casts' behavior is uniquely determined as follows: \ifshort (See the extende
 \end{theorem}
 In the case for an eager product $\times$, we can actually also show
 that running ${\dncast{\u F A_2}{\u F A_2'}{\ret x_2'}}$ and then
-${\dncast{\u F A_1}{\u F A_1'}{\ret x_2'}}$ is also an implementation of
+${\dncast{\u F A_1}{\u F A_1'}{\ret x_1'}}$ is also an implementation of
 this cast, and therefore equal to the above.  Intuively, this is
 sensible because the only effect a downcast introduces is a run-time
 error, and if either downcast errors, both possible implementations
@@ -3574,10 +3574,10 @@ These are equivalent to the CBPV translations of the standard CBV wrapping
 implementations; for example, the CBV upcast term
 $\lambda x'.\letXbeYinZ{\dncast{A_1}{A_1'}{x'}}{x}{\upcast{A_2}{A_2'}{(f x')}}$
 has its evaluation order made explicit, and the fact that its upcast is
-a (complex) value exposed.  In the downcast, CBPV term is free to
+a (complex) value exposed.  In the downcast, the GTT term is free to
 let-bind $(\upcast{A_1}{A_1'}{x})$ to avoid duplicating it, but because
-it is a (complex) value, it can also be substituted directly (which
-might expose reductions that can be optimized).
+it is a (complex) value, it can also be substituted directly, which
+might expose reductions that can be optimized.
 
 \begin{longonly}
 \subsection{Least Dynamic Types}
@@ -4053,7 +4053,7 @@ As a consequence we will also get consistency of dynamism:
 
 We break down this proof into 3 major steps.
 \begin{enumerate}
-\item (This section) We translate GTT into a statically typed \cbpvstar
+\item (This section) We translate GTT into a statically typed \cbpvstar\/
   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.
@@ -4113,11 +4113,10 @@ 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}.
 %
-We extended the inequational theory so that each term constructor for
-the recursive types is monotone, and with $\beta\eta$ axioms for them.
+We extend the inequational theory with monotonicity of each term constructor of
+the recursive types, and with their $\beta\eta$ rules.
 \begin{shortonly}
-The typing rules and equations for recursive types are in the the
-extended version.
+The rules for recursive types are in the extended version.
 \end{shortonly}
 
 \begin{longonly}
@@ -4287,8 +4286,8 @@ often occur more naturally in the following forms:
 \end{longproof}
 \end{longonly}
 
-Using this, and recalling the notion of ground type from
-Section~\ref{sec:upcasts-necessarily-values}, we define
+Using this, and using the notion of ground type from
+Section~\ref{sec:upcasts-necessarily-values} \emph{with $0$ and $\top$ removed}, we define
 
 \begin{definition}[Dynamic Type Interpretation]
   A $\dynv,\dync$ interpretation $\rho$ consists of (1) a
@@ -4444,7 +4443,7 @@ introduction forms for $\dynv$ are exactly the introduction forms for
 all of the value types (unit, pairing,$\inl$, $\inr$, $\force$), while
 elimination forms are all of the elimination forms for computation types
 ($\pi$, $\pi'$, application and binding); such ``bityped'' languages
-have been considered in \cite{ludics,zeilberger}.
+are related to \cite{girard01locussolum,zeilberger09thesis}.
 \begin{shortonly}
   In the extended version, we give an extension of GTT axiomatizing this
   implementation of the dynamic types.
@@ -4550,7 +4549,7 @@ type $\with$.
 Normally, these are not included in this way, but rather sums are
 encoded by making each case use a fresh constructor (using nominal
 techniques like opaque structs in Racket) and then making the sum the
-union of the constructors, as argued in (TODO: TH-Siek Wadlerfest).
+union of the constructors, as argued in \cite{siekth16recursiveunion}.
 %
 We leave modeling this nominal structure to future work, but in
 minimalist languages, such as simple dialects of Scheme and Lisp, sum
@@ -4652,7 +4651,7 @@ This leads to the following definition:
   $\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
-  isomorphic to a function that takes a list of \dynv as input ($(\mu
+  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
   arguments are passed individually on the stack, not as a

paper/max.bib

@@ -1035,3 +1035,28 @@ year="2014",
 pages="396--410",
 }
 
+@article{girard01locussolum,
+         title={Locus Solum: From the rules of logic to the logic of rules},
+         volume={11},
+         number={3},
+         journal={Mathematical Structures in Computer Science},
+         publisher={Cambridge University Press},
+         author={GIRARD, JEAN-YVES},
+         year={2001},
+         pages={301–506 }}
+
+@PhdThesis{zeilberger09thesis,
+  author =       {Noam Zeilberger},
+  title =        {The Logical Basis of Evaluation Order and Pattern-Matching. },
+  school =       {Carnegie Mellon University},
+  year =         {2009},
+}
+
+@Article{siekth16recursiveunion,
+  author =       {Jeremy Siek and Sam Tobin-Hochstadt},
+  title =        {The recursive union of some gradual types},
+  journal =      {A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Springer LNCS)},
+  year =         {2016},
+  volume =    {volume 9600},
+}
+