From ea6c0b6b6d7f8f42e7d020d6e647a3a435696bf1 Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Wed, 11 Jul 2018 19:01:52 -0400
Subject: [PATCH] make it fit
---
paper/gtt.tex | 46 +++++++++++++++++++++-------------------------
1 file changed, 21 insertions(+), 25 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 8227aa7..5620a44 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -9177,8 +9177,7 @@ $\errordivergerightop$ gives
$\Gamma \pipe \Delta \vDash E' \ix{\mathrel{\preceq\gtdyn}} \omega E \in \u B$.
\end{lemma}
-This, together with logical implies contextual equivalence, and a bit of
-massaging of the divergence preorders, gives the main theorem:
+This, together with logical implies contextual equivalence, gives the main theorem:
\begin{theorem}[Contextual Approximation/Equivalence Model CBPV] ~~\\
$\Gamma \pipe \Delta \vdash E \ltdyn E' : T$ implies
$\Gamma \pipe \Delta \vDash E \ctxize\ltdyn E' \in T$
@@ -9234,8 +9233,7 @@ differing syntactic type soundness theorems for different semantics of
gradual typing.
%
Our work here is complementary, showing that certain program
-equivalences can only be achieved by certain cast semantics, and giving
-a logic and semantics for verifying behavioral equivalences.
+equivalences can only be achieved by certain cast semantics.
\iflong
\paragraph{Gradual Typing Frameworks}
@@ -9268,33 +9266,31 @@ typing in the first place.
%
In fact, both systems \emph{fail} to preserve these equivalences.
%
-First, AGT reproduces the ``eager'' semantics of function casts,
-breaking the $\eta$ equality of functions.
+AGT reproduces the ``eager'' semantics of function casts,
+breaking $\eta$ for functions.
%
-Gradualizer, on the other hand, produces the ``lazy'' semantics and thus
-should validate the $\eta$ equality, though this does not seem to be a
-central component of the language: a different version of Gradualizer
-could produce the ``eager'' semantics and satisfy all of their criteria.
+Gradualizer produces the ``lazy'' semantics and thus should validate the
+$\eta$ equality, though this does not seem to be a central component of
+the language: a different version could produce the ``eager'' semantics
+and satisfy all of their criteria.
%
Both systems, however, fail to preserve the program equivalences of
parametric polymorphism, and in addition fail to meet gradual typing
criteria for stateful references.
%
-The ``reason'' that these violations occur is that they are not safety
-properties of the operational semantics, and the operational semantics
-is the only input to these frameworks.
+The ``reason'' that these violations occur isthat they are not safety
+properties of the operational semantics, which is the only input to
+these frameworks.
%
-While we have not yet considered these language features, we plan to
-apply our axiomatic approach to gradualizing polymorphism and state by
-starting with the rich \emph{relational logics and models} of program
-equivalence that have been developed for these
+In future work, we plan to apply our axiomatic approach to gradualizing
+polymorphism and state by starting with the rich \emph{relational logics
+ and models} of program equivalence for these
features~\cite{plotkinabadi93, dunphyphd, ahmed08:paramseal, neis09,
ahmed09:sdri}, which may lend insight into existing
-proposals~\cite{siek15:mono,ahmed17,igarashipoly17,siek-taha06}---
-for example, whether the
-``monotonic'' \citep{siek15:mono} and ``proxied'' \citep{siek-taha06}
-semantics of references support relational reasoning principles of
-local state.
+proposals~\cite{siek15:mono,ahmed17,igarashipoly17,siek-taha06}--- for
+example, whether the ``monotonic'' \citep{siek15:mono} and ``proxied''
+\citep{siek-taha06} semantics of references support relational reasoning
+principles of local state.
\iflong \paragraph{Blame}
\fi
@@ -9332,7 +9328,7 @@ so must blame the negative party.
%
In future work, we plan to investigate extensions of GTT with more than
one $\err$ with different blame labels, and an axiomatic account of
-a stronger, blame-aware observational equivalence.
+a blame-aware observational equivalence.
%% but our axiomatic language is
%% sufficiently similar to cast calculi that it should be easy to add.
@@ -9403,8 +9399,8 @@ sessions) with a dynamic value type and a dynamic session type.
However, their language is not \emph{polarized} in the same way as CBPV,
so there is not likely an analogue between our upcasts always being
between value types and downcasts always being between computation
-types. Instead, we could reconstruct this in a \emph{polarized} session
-type language like ~\cite{pfenninggriffith15session}.
+types. Instead, we might reconstruct this in a polarized session
+type language~\cite{pfenninggriffith15session}.
\begin{longonly}
The two dynamic types would then be the ``universal sender'' and
``universal receiver'' session types.
--
GitLab