related work on gradual session types

paper/gtt.tex

@@ -5582,6 +5582,30 @@ This gives some evidence that the specific choice of connectives of
 CBPV occupies a certain ``sweet spot'' between semantic expressivity
 and amenability to extensions.
 
+\paragraph{Modal Gradual Typing}
+
+The most similar gradually typed language to our full GTT is the
+language of gradual session types given in (TODO: cite Gradual Session
+Types).
+%
+It has several similarities: there are two sorts of types (values and
+sessions) and correspondingly two dynamic types: a dynamic value type
+and dynamic session type.
+%
+However, their formulation is quite different in that sessions are
+considered to be a \emph{subset} of value types whereas in ours there
+are explicit coercions between value and computation types.
+%
+Furthermore their language is not \emph{polarized} in the same way as
+CBPV, so there is not likely an analogue between our upcasts being
+always between value types and downcasts being always between
+computation types in their system.
+%
+Instead, we could reconstruct this in a \emph{polarized} session type
+language where there are two types of sessions: sending and receiving
+and there would be ``universal sender'' and ``universal receiver''
+session types.
+
 \paragraph{Dynamically Typed Call-by-push-value}
 
 Our interpretation of the dynamic types in CBPV suggests a design for