more intro

paper-new/intro.tex

@@ -236,6 +236,7 @@ corresponding technical reports having 50+ pages of proofs.
 % is tracked.
 \end{comment}
 
+\max{the stuff below is out of date}
 An alternative approach, which we investigate in this paper, is provided by
 \emph{synthetic guarded domain theory}\cite{birkedal-mogelberg-schwinghammer-stovring2011}.
 The techniques of synthetic guarded domain theory allow us to internalize the
@@ -260,7 +261,17 @@ The main contribution of this work is a categorical and denotational
 semantics for gradually typed langauges that models not just the term
 language but the graduality property as well.
 \begin{enumerate}
-\item First, we give a rational reconstruction \max{todo: more shit.}
+\item First, we give a simple abstract categorical model of GTT using CBPV double categories.
+\item Next, we modify this semantics to develop reflexive graph- and
+  double categorical models that abstract over the details of
+  step-indexed models, and provide a method for constructing such models.
+\item We instantiate the abstract construction to provide a concrete
+  semantics in informal guarded type theory which supports the
+  addition of arbitrary algebraic effects.
+\item We prove that the resulting denotational model is
+  \emph{adequate} for the graduality property: a closed term precision
+  $M \ltdyn N : \nat$ has the expected semantics, that $M$ errors or
+  $M$ and $N$ have the same extensional behavior.
 \end{enumerate}
 
 Our main contribution is a compositional denotational semantics for step-aware gradual typing,

paper-new/paper.tex

@@ -167,21 +167,4 @@
 \appendix
 \input{appendix}
 
-
-% \section{Discussion}\label{sec:discussion}
-
-% \subsection{Synthetic Ordering}
-
-% While the use of synthetic guarded domain theory allows us to very
-% conveniently work with non-well-founded recursive constructions while
-% abstracting away the precise details of step-indexing, we do work with
-% the error ordering in a mostly analytic fashion in that gradual types
-% are interpreted as sets equipped with an ordering relation, and all
-% terms must be proven to be monotone.
-% %
-% It is possible that a combination of synthetic guarded domain theory
-% with \emph{directed} type theory would allow for an a synthetic
-% treatment of the error ordering as well.
-
-
 \end{document}