diff --git a/paper/gtt.tex b/paper/gtt.tex
index 232ca3e8075719e5b103c34c91bcf475a1015797..626a7c0be8370f62e446a46ba303b0a7c3f4f5ba 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1559,13 +1559,35 @@ interpreted as value types in call-by-push-value.
\section{Theorems in Gradual Type Theory}
In this section, we derive equational and inequational properties of
-Gradual Type Theory. In what follows, ``unique'' means up to $\equidyn$.
+Gradual Type Theory.
-\subsection{Basic structure of GTT}
+In what follows, ``unique'' means up to term equidynamism $\equidyn$.
-GTT inherits a lot of stuff from CPBV, for example [TODO: cite CPBV book]
+\subsection{Inclusion of CBPV}
-\begin{lemma}[Initial objects] \label{lem:initial}
+Because the GTT term equidynamism relation includes the congruence and
+$\beta\eta$ axioms of call-by-push-value, the types inherit the
+universal properties they have there~\cite{cpbv}. We recall some
+relevant definitions and facts:
+
+\begin{definition}[Isomorphism] ~
+ \begin{enumerate}
+ \item We write $A \cong_v A'$ for a \emph{value isomorphism between
+ $A$ and $A'$}, which consists of two complex values $x : A \vdash V'
+ : A'$ and $x' : A' \vdash V : A$ such that $x : A \vdash V[V'/x']
+ \equidyn x : A$ and $x' : A' \vdash V'[V/x] \equidyn x' : A'$.
+ \item We write $\u B \cong_v \u B'$ for a \emph{computation
+ isomorphism between $\u B$ and $\u B'$}, which consists of two
+ complex stacls $\bullet : \u B \vdash S' : \u B'$ and $\bullet' : \u
+ B' \vdash S : \u B$ such that $\bullet : \u B \vdash S[S'/x']
+ \equidyn \bullet : \u B$ and $\bullet' : \u B' \vdash S'[S/\bullet]
+ \equidyn \bullet' : \u B'$.
+ \end{enumerate}
+\end{definition}
+
+\smallskip
+
+\begin{lemma}[Initial objects] ~ \label{lem:initial}
\begin{enumerate}
\item For all (value or computation) types $T$, there exists a unique
expression $x : 0 \vdash E : T$.
@@ -1579,7 +1601,7 @@ GTT inherits a lot of stuff from CPBV, for example [TODO: cite CPBV book]
\item $\u F 0$ is not provably \emph{strictly} initial among computation types.
\end{enumerate}
\end{lemma}
- \begin{proof}
+\begin{proof}~
\begin{enumerate}
\item Take $E$ to be $x : 0 \vdash \abort{x} : T$. Given any $E'$,
we have $E \equidyn E'$ by the $\eta$ principle for $0$.
@@ -1626,7 +1648,7 @@ GTT inherits a lot of stuff from CPBV, for example [TODO: cite CPBV book]
\end{enumerate}
\end{proof}
- \begin{lemma}[Terminal objects] \label{lem:terminal}
+ \begin{lemma}[Terminal objects] ~ \label{lem:terminal}
\begin{enumerate}
\item For any computation type $\u B$, there exists a unique stack
$\bullet : \u B \vdash S : \top$.
@@ -1638,7 +1660,7 @@ GTT inherits a lot of stuff from CPBV, for example [TODO: cite CPBV book]
\item $\top$ is not a strict terminal object.
\end{enumerate}
\end{lemma}
- \begin{proof}
+ \begin{proof} ~
\begin{enumerate}
\item Take $S = \{\}$. The $\eta$ rule for $\top$, $\bullet : \top
\vdash \bullet \equidyn \{\} : \top$, under the substitution of
@@ -1672,10 +1694,12 @@ GTT inherits a lot of stuff from CPBV, for example [TODO: cite CPBV book]
\subsection{Derived Cast Rules}
-Some helpful derived rules:
+The cast universal properties in Figure~\ref{fig:gtt-term-dyn-axioms}
+imply a number of seemingly more general rules for reasoning about
+casts, which will be helpful for the proofs below:
\begin{lemma}[Shifted Casts]
- The following are derivable
+ The following are derivable:
\begin{mathpar}
\inferrule
{\Gamma \pipe \Delta \vdash M : \u F A' \and A \ltdyn A'}
@@ -1688,7 +1712,7 @@ Some helpful derived rules:
\end{lemma}
\begin{proof}
They are instances of the general upcast and downcast rules, using the
- fact that $U$ and $\u F$ are congruences for type precision, so in the
+ fact that $U$ and $\u F$ are congruences for type dynamism, so in the
first rule $\u F A \ltdyn \u F A'$, and in the second, $U \u B \ltdyn
U \u B'$.
\end{proof}
@@ -1785,10 +1809,12 @@ $\dncast{\u B}{\u B''}{\bullet''}\ltdyn {\bullet''} : \u B \ltdyn \u B''$,
which is true by downcast left.
\end{proof}
-\subsection{Type-generic Cast Properties}
+\subsection{Type-generic Properties of Casts}
-\begin{theorem}{Casts (de)composition} \label{thm:decomposition}
- For any $A \ltdyn A' \ltdyn A''$ and $\u B \ltdyn \ltdyn \u B' \ltdyn \u B''$:
+The following results apply to casts in any types:
+
+\begin{theorem}[Casts (de)composition] \label{thm:decomposition}
+ For any $A \ltdyn A' \ltdyn A''$ and $\u B \ltdyn \u B' \ltdyn \u B''$:
\begin{enumerate}
\item $x : A \vdash \upcast A A x \equidyn x : A$
\item $x : A \vdash \upcast A {A''}x \equidyn \upcast{A'}{A''}\upcast A{A'} x : A''$
@@ -1799,7 +1825,7 @@ which is true by downcast left.
\end{enumerate}
\end{theorem}
-\begin{proof}
+\begin{proof} ~
\begin{enumerate}
\item To show $x : A \vdash \upcast A A x \ltdyn x$, by upcast left, it
suffices to show $x : A \vdash x \ltdyn x$, which is true by the
@@ -1853,7 +1879,7 @@ x : A \vdash \upcast{A}{\dynv}{x} \equidyn \upcast{A'}{\dynv}{\upcast{A}{A'}{x}}
\item $x : U \u B \vdash x \ltdyn \thunk{(\dncast{B}{B'}{(\force{(\upcast{U \u B}{U \u B'}{x})})})} : U \u B$
\end{enumerate}
\end{theorem}
-\begin{proof}
+\begin{proof} ~
\begin{enumerate}
\item By $\eta$ for $F$ types, $\bullet' : \u F A' \vdash \bullet'
\equidyn \bindXtoYinZ{\bullet'}{x'}{\ret{x'}} : \u F A'$, so it
@@ -1921,7 +1947,7 @@ x : A \vdash \upcast{A}{\dynv}{x} \equidyn \upcast{A'}{\dynv}{\upcast{A}{A'}{x}}
\end{proof}
In Figure~\ref{fig:gtt-term-dyn-axioms}, we asserted the retract axiom
-for casts into the dynamic type. More generally, we have
+for casts into the dynamic type. More generally:
\begin{theorem}[Retract Property for General Casts]
\begin{enumerate}
\item
@@ -1984,39 +2010,42 @@ for casts into the dynamic type. More generally, we have
The specification of upcasts and downcasts by their right and left
$\ltdyn$ rules defines them \emph{uniquely} up to $\equidyn$.
%
-In category-theoretic terms this says that the upcasts and downcasts
-have a \emph{universal property}, and so we can show that something
-else is equivalent to the upcast or downcast by showing that it has
-the \emph{same} property.
+In category-theoretic terms this says that ``being an upcast/downcast''
+is a \emph{universal property}, and so we can show that something else
+is equivalent to the upcast or downcast by showing that it has the
+\emph{same} property.
%
-\begin{theorem}[Specification for Casts is a Universal Property] \label{thm:casts-unique}
- If $A \ltdyn A'$ and $x : A \vdash V_u[x] : A'$ is a value such that
- the following judgments are provable:
+\begin{theorem}[Specification for Casts is a Universal Property]
+ ~ \label{thm:casts-unique}
+ \begin{enumerate}
+ \item
+ If $A \ltdyn A'$ and $x : A \vdash V[x] : A'$ is a value such that
\begin{mathpar}
\inferrule
{}
- {x : A \ltdyn x' : A' \vdash V_u[x] \ltdyn x' : A'}
+ {x : A \ltdyn x' : A' \vdash V[x] \ltdyn x' : A'}
\inferrule
{}
- {x_2 : A \ltdyn x : A \vdash x_2 \ltdyn V_u[x] : A \ltdyn A'}
+ {x_2 : A \ltdyn x : A \vdash x_2 \ltdyn V[x] : A \ltdyn A'}
\end{mathpar}
+ then $x : A \vdash V \equidyn x : A$.
- then we can prove $x : A \vdash V_u[x] \equidyn x : A$.
-
- Similarly, if $\u B \ltdyn \u B'$ and $\bullet : \u B' \vdash S_d :
- \u B$ is a stack such that the following are provable:
+ \item
+ If $\u B \ltdyn \u B'$ and $\bullet : \u B' \vdash S :
+ \u B$ is a stack such that
\begin{mathpar}
\inferrule
{}
- {\bullet \ltdyn \bullet : \u B' \vdash S_d \ltdyn \bullet : \u B \ltdyn \u B'}
+ {\bullet \ltdyn \bullet : \u B' \vdash S \ltdyn \bullet : \u B \ltdyn \u B'}
\inferrule
{}
- {\bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn S_d : \u B}
+ {\bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn S : \u B}
\end{mathpar}
- then we can prove $\bullet : \u B' \vdash S_d \equidyn \dncast{\u B}{\u B'}\bullet : \u B$
+ then $\bullet : \u B' \vdash S \equidyn \dncast{\u B}{\u B'}\bullet : \u B$
+ \end{enumerate}
\end{theorem}
\begin{proof}
\begin{mathpar}
@@ -2252,7 +2281,7 @@ Dually, we have
\end{proof}
-\begin{theorem}[Functorial Casts]
+\begin{theorem}[Functorial Casts] \label{thm:functorial-casts}
\begin{small}
\[
\begin{array}{l}
@@ -3021,7 +3050,8 @@ upcasts and value downcasts as well.
Some value downcasts and computation upcasts do exist, leading to a
characterization of the casts for the monad/comonad of $F \dashv U$:
-\begin{theorem} Suppose $A \ltdyn A'$ and $\u B \ltdyn \u B'$.
+\begin{theorem}[Monadic/Comonadic Casts] \label{thm:monadic-comonadic-casts}
+ Suppose $A \ltdyn A'$ and $\u B \ltdyn \u B'$.
\begin{enumerate}
\item $\bullet : \u F A \vdash
\bindXtoYinZ{\bullet}{x:A}{\ret{(\upcast{A}{A'}{x})}} : \u F A'$
@@ -3173,7 +3203,7 @@ characterization of the casts for the monad/comonad of $F \dashv U$:
\]
\end{definition}
-\begin{definition}[Ground type precision]
+\begin{definition}[Ground type dynamism]
Let $A \ltdyn' A'$ and $\u B \ltdyn' \u B'$ be the relations defined
by the rules in Figure~\ref{fig:gtt-type-dynamism-and-terms}
with the axioms $A \ltdyn \dynv$ and $\u B \ltdyn \dync$ restricted to
@@ -3196,7 +3226,7 @@ transitivity, so $\u F A \ltdyn \u F \dynv$ by congruence, which is
ground.
\end{proof}
-\begin{lemma}[Alternative Characterization of Type Precision]
+\begin{lemma}[Alternative Characterization of Type Dynamism]
$A \ltdyn A'$ iff $A \ltdyn' A'$ and $\u B \ltdyn \u B'$ iff $\u B
\ltdyn' \u B'$
\end{lemma}
@@ -3212,17 +3242,133 @@ G$, and then use transitivity with $G \ltdyn \dynv$ and $\u G \ltdyn
\dync$.
\end{proof}
+In GTT, we assert that all value upcasts and computation downcasts
+exist, but we can consider sub-theories of GTT where not all casts are
+assumed a priori to exist.
+
+\begin{lemma}[Casts are Admissible] \label{lem:casts-admissible}
+Suppose we restrict the postulated casts to those between ground types
+and the dynamic type or between the shifts of those: we have values
+$x : G \vdash \upcast{G}{\dynv}{x} : \dynv$ and
+$\bullet : \u F \dynv \vdash \dncast{\u F G}{\u F \dynv}{x} : \u F \dynv$ and
+$\bullet : \dync \vdash \dncast{\u G}{\dync}{\bullet} : \dync$ and
+$x : U \u G \vdash \upcast{U \u G}{U \dync}{x} : U \dync$
+satisfying the universal
+properties of upcasts and downcasts respectively, but no other casts are
+stipulated to exist. Then it is admissible that
+\begin{enumerate}
+\item for every type dynamism $A \ltdyn A'$
+ there is a definable upcast $\defupcast{A}{A'}$
+ and a definable downcast $\defdncast{\u F A}{\u F A'}$
+\item for every type
+dynamism $\u B \ltdyn \u B'$ there is a definable downcast
+$\defdncast{\u B}{\u B'}$ and a definavle upcast
+$\defdncast{U \u B}{U \u B'}$
+\end{enumerate}
+\end{lemma}
-
-\begin{theorem}{Upcasts are (Complex) Values, Downcasts are (Complex) Stacks}
- If the tagging upcasts are complex values and untagging downcasts
- are stacks, then all upcasts are complex values and all downcasts
- are complex stacks.
-\end{theorem}
\begin{proof}
+ By induction on type dynamism $A \ltdyn' A'$ and $\u B \ltdyn' \u B'$.
+
+ To streamline the exposition above, we stated
+ Theorem~\ref{thm:decomposition} and Theorem~\ref{thm:functorial-casts}
+ as showing that the ``definitions'' of each cast are equidynamic with
+ the postulated cast (e.g. $\upcast{A}{A''} \equidyn
+ \upcast{A'}{A''}{\upcast{A}{A'}}$). However, the proofs given do not
+ rely on any axioms of GTT besides the universal properties of the
+ ``smaller'' casts used in the definition and the $\beta\eta$ rules for
+ the relevant types. Thus, the same proofs can be read as showing that
+ the ``definitions'' of the casts have the correct universal property,
+ whether or not a cast with that universal property is a priori
+ asserted to exist. So these proofs are essentially the inductive
+ steps here.
+
+ We show a few representative cases:
+
+ In the cases for $G \ltdyn \dynv$ or $\u G \ltdyn \dync$, we have
+ assumed appropriate casts $\upcast{G}{\dynv}$ and
+ $\dncast{\u F G}{\u F \dynv}$ and
+ $\dncast{\u G}{\dync}$ and
+ $\upcast{U \u G}{U \dync}$.
+
+ In the case for identity $A \ltdyn A$, we need to show that there is
+ an upcast $\defupcast{A}{A}$ and a downcast $\defdncast{\u F A}{\u F A}$
+ The proof of Theorem~\ref{thm:decomposition} shows that the identity
+ value and stack have the correct universal property.
+
+ In the case where type dynamism was concluded by
+ transitivity between $A \ltdyn A'$ and $A' \ltdyn A''$, by the
+ inductive hypotheses we get upcasts $\defupcast{A}{A'}$ and
+ $\defupcast{A'}{A''}$, and the proof of
+ Theorem~\ref{thm:decomposition} shows that defining
+ $\defupcast{A}{A''}$ to be $\defupcast{A'}{A''}{\defupcast{A}{A'}}$
+ has the correct universal property. For the downcast, we get
+ $\defdncast{\u F A}{\u F A'}$ and
+ $\defdncast{\u F A'}{\u F A''}$ by the inductive hypotheses, and the
+ proof of Theorem~\ref{thm:decomposition} shows that their composition
+ has the correct universal property.
+ In the case where type dynamism was concluded by the congruence rule
+ for $A_1 + A_2 \ltdyn A_1' + A_2'$ from $A_i \ltdyn A_i'$, we have
+ upcasts $\defupcast{A_i}{A_i'}$ and downcasts $\defdncast{\u F A_i}{\u F A_i'}$
+ by the inductive hypothesis, and the proof of
+ Theorem~\ref{thm:decomposition} shows that
+ \[
+ \begin{array}{c}
+ \bindXtoYinZ{\bullet}{(s : (A_1' + A_2'))}{}\\
+ {\caseofXthenYelseZ{s}
+ {x_1'.\bindXtoYinZ{(\defdncast{\u F A_1}{\u F A_1'}{(\ret{x_1'})})}{x_1}{\ret{(\inl {x_1})}}}
+ {x_2'.\bindXtoYinZ{(\defdncast{\u F A_2}{\u F A_2'}{(\ret{x_2'})})}{x_2}{\ret{(\inr {x_2})}}}}
+ \end{array}
+ \]
+ have the desired universal property.
+
+ In the case where type dynamism was concluded by the congruence rule
+ for $\u F A \ltdyn \u F A'$ from $A \ltdyn A'$, we obtain by induction
+ a \emph{upcast} $A \ltdyn A'$ and a downcast $\defdncast{\u F A}{\u F A'}$
+ We need a
+ \emph{downcast} $\defdncast{\u F A}{F A'}$, which we have,
+ and an \emph{upcast} $\defdncast{U \u F A}{U \u F A'}$, which is
+ constructed as in Theorem~\ref{thm:monadic-comonadic-casts}.
\end{proof}
+The following theorem shows that there is no loss of generality in
+postulating that all upcasts are values and all downcasts are stacks,
+assuming that the basic upcasts and downcasts between ground types and
+the dynamic types are such (which they are in the model constructed
+below): \emph{any} monadic upcast/comonadic downcast is pure, in the
+sense that it is the (co)monadic lift of a value upcast/stack downcast.
+\begin{theorem}[Upcasts are Necessarily Values, Downcasts are Necessarily Stacks]
+ Suppose we postulate the casts between ground types and the dynamic
+ type (and the shifts thereof) as complex values/stacks as in
+ Lemma~\ref{lem:casts-admissible}: $x : G \vdash \upcast{G}{\dynv}{x} :
+ \dynv$ and $\bullet : \u F \dynv \vdash \dncast{\u F G}{\u F \dynv}{x}
+ : \u F \dynv$ and $\bullet : \dync \vdash \dncast{\u
+ G}{\dync}{\bullet} : \dync$ and $x : U \u G \vdash \upcast{U \u G}{U
+ \dync}{x} : U \dync$.
+ Suppose further that for every type precision $A \ltdyn A'$ we
+ postulate an upcast $\upcast{U \u F A}{U \u F A'}$,
+ and for every type precsion $\u B \ltdyn \u B'$ a downcast
+ $\dncast{\u F U \u B}{\u F U \u B'}$.
+ Then there exists a value upcast $\defupcast{A}{A'}$ and a stack
+ downcast $\defdncast{\u B}{\u B'}$ such that
+ \[
+ \begin{array}{c}
+ x : U \u F A \vdash \upcast{U \u F A}{U \u F A'}{x} \equidyn \thunk{ (\bindXtoYinZ{{\force x}}{x:A}{\ret{(\defupcast{A}{A'}{x})}})}\\
+ \bullet : \u F U \u B' \vdash \dncast{\u F U \u B}{\u F U \u B'}{\bullet} \equidyn
+ \bindXtoYinZ{\bullet}{x':U \u B'}{\ret{(\thunk{(\defdncast{\u B}{\u B'}{(\force x)})})}}
+ \end{array}
+ \]
+\end{theorem}
+\begin{proof}
+Lemma~\ref{lem:casts-admissible} constructs $\defupcast{A}{A'}$ and
+$\defdncast{\u B}{\u B'}$, so the proof of
+Theorem~\ref{thm:monadic-comonadic-casts} gives the result (as with
+other arguments in this section, it is only necessary to observe that
+the proof really shows that the definitions of the casts have the
+correct universal property, without relying on a cast with that
+universal property already existing).
+\end{proof}
\subsection{Equidynamic Types are Isomorphic}
@@ -8249,6 +8395,8 @@ invoked with any finite number of arguments on the stack, a fairly
accurate model of implementations of Scheme that pass multiple
arguments on the stack.
+\bibliography{max}
+
\appendix
\section{Program Equivalences and Inequivalences in Previous Work}
diff --git a/paper/max.bib b/paper/max.bib
new file mode 100644
index 0000000000000000000000000000000000000000..f70e5d4218848590882de70b5adb40de0ab42905
--- /dev/null
+++ b/paper/max.bib
@@ -0,0 +1,977 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%% String Definitions %%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Publishing houses
+% %%%%%%%%%%%%%%%%%
+@STRING{ap = "Academic Press" }
+@STRING{springer = {Springer-Verlag} }
+@STRING{lncs = "Lecture Notes in Computer Science" }
+@STRING{lnm = "Lecture Notes in Mathematics" }
+@STRING{gtm = "Graduate Texts in Mathematics" }
+@STRING{lfcs = "Laboratory for Foundations of Computer Science,
+ University of Edinburgh" }
+@STRING{mp = "MIT Press" }
+@STRING{mitpress = mp }
+%
+% Journals and magazines
+% %%%%%%%%%%%%%%%%%%%%%%
+@STRING{toplas = "ACM Transactions on Programming Languages and Systems" }
+@STRING{jlp = {Journal of Logic Programming} }
+@STRING{cacm = "Communications of the {ACM}" }
+@STRING{jacm = "Journal of the {ACM}" }
+@STRING{tcs = "Theoretical Computer Science" }
+@STRING{jsl = "Journal of Symbolic Logic" }
+@STRING{siamjc = "SIAM Journal on Computing" }
+@STRING{mscs = "Mathematical Structures in Computer Science" }
+@STRING{proc = "Proceedings of the" }
+@STRING{ic = "Information and Computation" }
+@STRING{iandcomp = {Information and Computation} }
+@string{ifip = "International Federation for Information Processing World Computer Congress (IFIP)"}
+@STRING{jfp = "Journal of Functional Programming" }
+@STRING{lmcs = "Logical Methods in Computer Science" }
+@string{hosc = "Higher-Order and Symbolic Computation"}
+@STRING{cup = "Cambridge University Press" }
+@STRING{mcgh = "McGraw-Hill" }
+@STRING{nh = "North Holland" }
+@STRING{sv = "Springer-Verlag" }
+@STRING{aw = "Addison-Wesley" }
+@STRING{ph = "Prentice Hall" }
+@STRING{signot = "SIGPLAN Notices"}
+@STRING{taoop = "Carl A. Gunter and John C. Mitchell, editors, {\em
+ Theoretical Aspects of Object-Oriented Programming:
+ Types, Semantics, and Language Design}, MIT Press, 1994" }
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Conferences %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+@STRING{popl = "{ACM} {S}ymposium on {P}rinciples of {P}rogramming
+ {L}anguages ({POPL})" }
+@STRING{popl73 = popl # ", Boston, Massachusetts" }
+@STRING{popl75 = popl # ", Palo Alto, California" }
+@STRING{popl76 = popl # ", {A}tlanta, {G}eorgia" }
+@STRING{popl77 = popl # ", Los Angeles, California" }
+@STRING{popl78 = popl # ", Tucson, Arizona" }
+@STRING{popl79 = popl # ", San Antonio, Texas" }
+@STRING{popl80 = popl # ", Las Vegas, Nevada" }
+@STRING{popl81 = popl # ", Williamsburg, Virginia" }
+@STRING{popl82 = popl # ", Albuquerque, New Mexico" }
+@STRING{popl83 = popl # ", Austin, Texas" }
+@STRING{popl84 = popl # ", Salt Lake City, Utah" }
+@STRING{popl85 = popl # ", New Orleans, Louisiana" }
+@STRING{popl86 = popl # ", St.\ Petersburg Beach, Florida" }
+@STRING{popl87 = popl # ", Munich, Germany" }
+@STRING{popl88 = popl # ", San Diego, California" }
+@STRING{popl89 = popl # ", Austin, Texas" }
+@STRING{popl90 = popl # ", {S}an {F}rancisco, {C}alifornia" }
+@STRING{popl91 = popl # ", Orlando, Florida" }
+@STRING{popl92 = popl # ", Albuquerque, New Mexico" }
+@STRING{popl93 = popl # ", Charleston, South Carolina" }
+@STRING{popl94 = popl # ", {P}ortland, {O}regon" }
+@STRING{popl95 = popl # ", San Francisco, California" }
+@STRING{popl96 = popl # ", St.~Petersburg Beach, Florida" }
+@STRING{popl97 = popl # ", Paris, France" }
+@STRING{popl98 = popl # ", San Diego, California" }
+@STRING{popl99 = popl # ", San Antonio, Texas" }
+@STRING{popl00 = popl # ", Boston, Massachusetts" }
+@STRING{popl01 = popl # ", London, England" }
+@STRING{popl02 = popl # ", Portland, Oregon" }
+@STRING{popl03 = popl # ", New Orleans, Louisiana" }
+@STRING{popl04 = popl # ", Venice, Italy" }
+@STRING{popl05 = popl # ", Long Beach, California" }
+@STRING{popl06 = popl # ", Charleston, South Carolina" }
+@STRING{popl07 = popl # ", Nice, France" }
+@STRING{popl08 = popl # ", San Francisco, California" }
+@STRING{popl09 = popl # ", Savannah, Georgia" }
+@STRING{popl10 = popl # ", Madrid, Spain" }
+@STRING{popl11 = popl # ", Austin, Texas" }
+@STRING{popl12 = popl # ", Philadelphia, Pennsylvania" }
+@STRING{popl13 = popl # ", Rome, Italy" }
+@STRING{popl14 = popl # ", San Diego, California" }
+@STRING{popl15 = popl # ", Mumbai, India" }
+@STRING{popl16 = popl # ", St. Petersburg, Florida" }
+% ----
+@STRING{icfp = "{I}nternational {C}onference on {F}unctional {P}rogramming
+ ({ICFP})" }
+@STRING{icfp96 = icfp # ", Philadelphia, Pennsylvania" }
+@STRING{icfp97 = icfp # ", Amsterdam, The Netherlands" }
+@STRING{icfp98 = icfp # ", Baltimore, Maryland, USA" }
+@STRING{icfp99 = icfp # ", Paris, France" }
+@STRING{icfp00 = icfp # ", Montreal, Canada" }
+@STRING{icfp01 = icfp # ", Firenze, Italy" }
+@STRING{icfp02 = icfp # ", Pittsburgh, Pennsylvania" }
+@STRING{icfp03 = icfp # ", Uppsala, Sweden" }
+@STRING{icfp04 = icfp # ", Snowbird, Utah" }
+@STRING{icfp05 = icfp # ", Tallinn, Estonia" }
+@STRING{icfp06 = icfp # ", Portand, Oregon" }
+@STRING{icfp07 = icfp # ", Freiburg, Germany" }
+@STRING{icfp08 = icfp # ", Victoria, British Columbia, Canada" }
+@STRING{icfp09 = icfp # ", Edinburgh, Scotland" }
+@STRING{icfp10 = icfp # ", Baltimore, Maryland" }
+@STRING{icfp11 = icfp # ", Tokyo, Japan" }
+@STRING{icfp12 = icfp # ", Copenhagen, Denmark" }
+@STRING{icfp13 = icfp # ", Boston, Massachusetts" }
+@STRING{icfp14 = icfp # ", Gothenburg, Sweden" }
+@STRING{icfp15 = icfp # ", Vancouver, British Columbia, Canada" }
+@STRING{icfp16 = icfp # ", Nara, Japan" }
+@STRING{icfp17 = icfp # ", Oxford, United Kingdom" }
+
+% ----
+@STRING{oopsla = "{ACM} {S}ymposium on {O}bject {O}riented {P}rogramming:
+ {S}ystems, {L}anguages, and {A}pplications ({OOPSLA})" }
+@STRING{oopsla86 = oopsla # ", Portland, Oregon" }
+@STRING{oopsla89 = oopsla }
+@STRING{oopsla98 = oopsla # ", Vancouver, British Columbia" }
+@STRING{oopsla08 = oopsla # ", Nashville, Tennessee" }
+% ----
+@STRING{lics = "IEEE Symposium on Logic in Computer Science (LICS)" }
+@STRING{lics91 = lics # ", Amsterdam, The Netherlands" }
+@STRING{lics92 = lics # ", Santa Cruz, California" }
+@STRING{lics93 = lics # ", Montreal, Canada" }
+@STRING{lics94 = lics # ", Paris, France" }
+@STRING{lics95 = lics # ", San Diego, California" }
+@STRING{lics96 = lics # ", New Brunswick, New Jersey" }
+@STRING{lics97 = lics # ", Warsaw, Poland" }}
+@STRING{lics98 = lics # ", Indianapolis, Indiana" }
+@STRING{lics99 = lics # ", Trento, Italy" }
+@STRING{lics00 = lics # ", Santa Barbara, California" }
+@STRING{lics01 = lics # ", Boston, Massachusetts" }
+@STRING{lics02 = lics # ", Copenhagen, Denmark" }
+@STRING{lics03 = lics # ", Ottawa, Canada" }
+@STRING{lics04 = lics # ", Turku, Finland" }
+@STRING{lics05 = lics # ", Chicago, Illinois" }
+@STRING{lics06 = lics # ", Seattle, Washington" }
+@STRING{lics07 = lics # ", Wroclaw, Poland" }
+@STRING{lics08 = lics # ", Pittsburgh, Pennsylvania" }
+@STRING{lics09 = lics # ", Los Angeles, California" }
+@STRING{lics10 = lics # ", Edinburgh, Scotland" }
+@STRING{lics11 = lics # ", Toronto, Canada" }
+@STRING{lics12 = lics # ", Dubrovnik, Croatia" }
+@STRING{lics13 = lics # ", New Orleans, Louisiana" }
+@STRING{lics14 = lics # ", Vienna, Austria" }
+% ----
+@STRING{pldi = "{ACM SIGPLAN Conference on Programming Language Design
+ and Implementation (PLDI)}" }
+@STRING{pldi88 = pldi # ", {A}tlanta, {G}eorgia" }
+@STRING{pldi89 = pldi # ", Portland, Oregon" }
+@STRING{pldi90 = pldi # ", White Plains, New York" }
+@STRING{pldi91 = pldi # ", Toronto, Ontario" }
+@STRING{pldi92 = pldi # ", San Francisco, California" }
+@STRING{pldi93 = pldi # ", Albuquerque, New Mexico" }
+@STRING{pldi94 = pldi # ", Orlando, Florida" }
+@STRING{pldi95 = pldi # ", La Jolla, California" }
+@STRING{pldi96 = pldi # ", Philadephia, Pennsylvania" }
+@STRING{pldi97 = pldi # ", Las Vegas, Nevada" }
+@STRING{pldi98 = pldi # ", {M}ontreal, {C}anada" }
+@STRING{pldi99 = pldi # ", {A}tlanta, {G}eorgia" }
+@STRING{pldi00 = pldi # ", Vancouver, British Columbia, Canada" }
+@STRING{pldi01 = pldi # ", Snowbird, Utah" }
+@STRING{pldi02 = pldi # ", Berlin, Germany" }
+@STRING{pldi03 = pldi # ", San Diego, California" }
+@STRING{pldi04 = pldi # ", Washington, DC" }
+@STRING{pldi05 = pldi # ", Chicago, Illinois" }
+@STRING{pldi06 = pldi # ", Ottawa, Canada" }
+@STRING{pldi07 = pldi # ", San Diego, California" }
+@STRING{pldi08 = pldi # ", Tucson, Arizona" }
+@STRING{pldi09 = pldi # ", Dublin, Ireland" }
+@STRING{pldi10 = pldi # ", Toronto, Canada" }
+@STRING{pldi11 = pldi # ", San Jose, California" }
+@STRING{pldi12 = pldi # ", Beijing, China" }
+@STRING{pldi13 = pldi # ", Seattle, Washington" }
+@STRING{pldi14 = pldi # ", Edinburgh, Scotland" }
+% ----
+@STRING{lfp = "ACM Symposium on Lisp and Functional Programming (LFP)" }
+@STRING{lfp84 = lfp # ", Austin, Texas" }
+@STRING{lfp88 = lfp # ", Snowbird, Utah" }
+@STRING{lfp90 = lfp }
+@STRING{lfp92 = lfp }
+% ----
+@STRING{fpca = "ACM Symposium on Functional Programming Languages and
+ Computer Architecture (FPCA)" }
+@STRING{fpca89 = fpca }
+@STRING{fpca93 = fpca }
+% ----
+@STRING{sosp=" {ACM} {S}ymposium on {O}perating {S}ystems {P}rinciples ({SOSP})"}
+% ----
+@STRING{fool = "Workshop on Foundations of Object-Oriented Languages
+ (FOOL), informal proceedings" }
+@STRING{tlca = "Typed Lambda Calculi and Applications (TLCA)" }
+@STRING{tlca93 = tlca # ", Utrecht, The Netherlands" }
+@STRING{tlca95 = tlca # ", Edinburgh, UK" }
+@STRING{tlca97 = tlca # ", Nancy, France" }
+@STRING{tlca99 = tlca # ", L'Aquila, Italy" }
+@STRING{tlca01 = tlca # ", Krakow, Poland" }
+@STRING{tlca03 = tlca # ", Valencia, Spain" }
+@STRING{tlca05 = tlca # ", Nara, Japan" }
+@STRING{tlca07 = tlca # ", Paris, France" }
+@STRING{tlca09 = tlca # ", Brasilia, Brazil" }
+@STRING{tlca11 = tlca # ", Novi Sad, Serbia" }
+@STRING{tlca13 = tlca # ", Eindhoven, The Netherlands" }
+
+@string{cav = "Conference on Computer Aided Verification (CAV)"}
+@string{ccs = "ACM Conference on Computer and Communication Security (CCS)"}
+@string{oakland = "{IEEE} Symposium on Security and Privacy"}
+@string{dls = "Dynamic Languages Symposium (DLS)"}
+@STRING{esop = "European Symposium on Programming (ESOP)" }
+@STRING{esop92 = esop # ", Rennes, France" }
+@STRING{ecoop = "{E}uropean {C}onference on {O}bject-{O}riented
+ {P}rogramming ({ECOOP})" }
+@STRING{ecoop97 = ecoop }
+@STRING{ecoop02 = ecoop # ", Malaga, Spain" }
+@STRING{flops = "International Symposium on Functional and Logic Programming (FLOPS)" }
+@STRING{flops02 = flops # ", Aizu, Japan" }
+@string{icalp = "International Colloquium on Automata, Languages and Programming (ICALP)"}
+@string{plpv = "Programming Languages meets Program Verification (PLPV)"}
+@STRING{post = "Principles of Security and Trust (POST)" }
+@string{ppdp = "ACM Conference on Principles and Practice of Declarative Programming (PPDP)"}
+@string{scheme = "Scheme and Functional Programming Workshop (Scheme)"}
+@string{stop = "Workshop on Script-to-Program Evolution (STOP)"}
+@string{tldi = "ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI)"}
+@STRING{tacs = "Theoretical Aspects of Computer Software (TACS)" }
+@STRING{tacs01 = tacs # ", Sendai, Japan" }
+@string{tfp = "Trends in Functional Programming (TFP)"}
+@STRING{webdb = {International Workshop on the Web and Databases
+ (WebDB)} }
+@STRING{langsec = "Language-theoretic Security IEEE Security and Privacy Workshop (LangSec)"}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+@incollection{scott71,
+ title={Continuous lattices},
+ author={Scott, Dana},
+ booktitle={Toposes, algebraic geometry and logic},
+ pages={97--136},
+ year={1972},
+}
+
+@article{scott76,
+ title={Data types as lattices},
+ author={Scott, Dana},
+ journal={Siam Journal on computing},
+ volume={5},
+ number={3},
+ pages={522--587},
+ year={1976},
+ publisher={SIAM}
+}
+
+@inproceedings{wadler-findler09,
+ author = "Philip Wadler and Robert Bruce Findler",
+ title = "Well-typed programs can't be blamed",
+ booktitle = esop,
+ year = 2009,
+ month = mar,
+ pages = "1--16",
+ location = "York, UK"
+}
+
+@inproceedings{tobin-hochstadt06,
+ author = "Sam Tobin-Hochstadt and Matthias Felleisen",
+ title = "Interlanguage Migration: From Scripts to Programs",
+ booktitle = dls,
+ month = oct,
+ pages = "964--974",
+ year = 2006,
+}
+
+@inproceedings{tobin-hochstadt08,
+ author = {Sam Tobin-Hochstadt and Matthias Felleisen},
+ title = {The Design and Implementation of Typed Scheme},
+ booktitle = popl08,
+ year = {2008}}
+
+@inproceedings{siek-taha06,
+ author = "Jeremy G. Siek and Walid Taha",
+ title = "Gradual Typing for Functional Languages",
+ booktitle = scheme,
+ month = sep,
+ pages = "81--92",
+ year = 2006
+}
+
+@inproceedings{scott80,
+ author="Dana S. Scott",
+ booktitle="To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism",
+ editor="J.P. Seldin and J.R. Hindley",
+ title="Relating Theories of the Lambda-Calculus",
+ year=1980,
+ pages="403--450"}
+
+@inproceedings{findler-felleisen02,
+author = {Robert Bruce Findler and Matthias Felleisen},
+title = {Contracts for higher-order functions},
+booktitle = icfp,
+year = {2002},
+month = sep,
+pages = {48--59}
+}
+
+@inproceedings{findler-blume06,
+ author = "Robby Findler and Matthias Blume",
+ title = "Contracts as Pairs of Projections",
+ booktitle = flops,
+ month = apr,
+ year = 2006,
+}
+@inproceedings{siek-wadler10,
+ author = {Jeremy G. Siek and Philip Wadler},
+ title = {Threesomes, with and without blame},
+ booktitle = popl,
+ pages = {365--376},
+ year = {2010},
+}
+
+@inproceedings{longley03,
+ title={Universal types and what they are good for},
+ author={Longley, John R},
+ booktitle={Domain theory, logic and computation},
+ pages={25--63},
+ year={2003},
+}
+@inproceedings{dimoulas12,
+title = "Complete Monitors for Behavioral Contracts",
+author = "Christos Dimoulas and Sam Tobin-Hochstadt and Matthias Felleisen",
+booktitle = esop,
+year = 2012,
+month = mar}
+@inproceedings{mz2015functors,
+ author = {Melli\`{e}s, Paul-Andr{\'e} and Zeilberger, Noam},
+ title = {Functors Are Type Refinement Systems},
+ booktitle = {Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ series = {POPL '15},
+ year = {2015},
+ isbn = {978-1-4503-3300-9},
+ location = {Mumbai, India},
+ pages = {3--16},
+ numpages = {14},
+ url = {http://doi.acm.org/10.1145/2676726.2676970},
+ doi = {10.1145/2676726.2676970},
+ acmid = {2676970},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {category theory, refinement types, type theory},
+}
+@article{mz2015isbellpreprint,
+ author = {Paul{-}Andr{\'{e}} Melli{\`{e}}s and
+ Noam Zeilberger},
+ title = {Isbell Duality for Refinement Types},
+ journal = {CoRR},
+ volume = {abs/1501.05115},
+ year = {2015},
+ url = {http://arxiv.org/abs/1501.05115},
+ timestamp = {Mon, 02 Feb 2015 14:12:25 +0100},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/MelliesZ15},
+ bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+@inproceedings{mz2016bifibrational,
+ author = {Paul{-}Andr{\'{e}} Melli{\`{e}}s and
+ Noam Zeilberger},
+ title = {A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine},
+ booktitle = {Proceedings of the 31st Annual {ACM/IEEE} Symposium on Logic in Computer
+ Science, {LICS} '16, New York, NY, USA, July 5-8, 2016},
+ pages = {555--564},
+ year = {2016},
+ crossref = {DBLP:conf/lics/2016},
+ url = {http://doi.acm.org/10.1145/2933575.2934525},
+ doi = {10.1145/2933575.2934525},
+ timestamp = {Thu, 27 Oct 2016 11:27:54 +0200},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/lics/MelliesZ16},
+ bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+
+@article{shulman2008framed,
+ title={Framed bicategories and monoidal fibrations},
+ author={Shulman, Michael},
+ journal={Theory and Applications of Categories},
+ volume={20},
+ number={18},
+ pages={650--738},
+ year={2008}
+}
+
+@article{courser2016bicategory,
+ title={A bicategory of decorated cospans},
+ author={Courser, Kenny},
+ journal={arXiv preprint arXiv:1605.08100},
+ year={2016}
+}
+
+@article{garner2006,
+author = {Garner, Richard},
+journal = {Cahiers de Topologie et Géométrie Différentielle Catégoriques},
+number = 4,
+pages = {261-317},
+title = {Double clubs},
+volume = 47,
+year = 2006,
+}
+
+@misc{shulman2009lax,
+ title = {The Problem with Lax Functors},
+ author = {Shulman, Mike},
+ howpublished = {\url{https://golem.ph.utexas.edu/category/2009/12/the_problem_with_lax_functors.html}},
+ note = {Accessed: 2016-11-22},
+}
+
+@misc{harley,
+ title = {The Combination of Dynamic and Static Typing from a Categorical Perspective},
+ author = {Harley Eades III and Michael Townsend},
+ howpublished = {\url{http://metatheorem.org/includes/pubs/Grady-Draft.pdf}},
+ year={2017},
+ note = {Accessed: 2017-7-7},
+}
+
+
+@article{hayashi85,
+ author = {Susumu Hayashi},
+ title = {Adjunction of Semifunctors: Categorical Structures in Nonextensional
+ Lambda Calculus},
+ journal = {Theor. Comput. Sci.},
+ volume = {41},
+ pages = {95--104},
+ year = {1985},
+}
+
+@article{felleisen90,
+ title={On the expressive power of programming languages},
+ author={Felleisen, Matthias},
+ journal={ESOP'90},
+ year={1990},
+}
+@article{benton05:embedded,
+ title={Embedded Interpreters},
+ author={Nick Benton},
+ journal=jfp,
+ volume={15},
+ number={04},
+ pages={503--542},
+ year={2005},
+ publisher={Cambridge Univ Press}
+}
+@article{henglein94:dynamic-typing,
+ author="Fritz Henglein",
+ title="Dynamic Typing: Syntax and Proof Theory",
+ journal=scp,
+ volume="22",
+ number="3",
+ pages="197--230",
+ year="1994"
+}
+@article{favonia17,
+ title={Correctness of compiling polymorphism to dynamic typing},
+ volume={27},
+ journal={Journal of Functional Programming},
+ author={Keun-Bang Hou (Favonia) and Nick Benton and Robert Harper},
+ year={2017}
+}
+@inproceedings{AGT,
+ author = {Garcia, Ronald and Clark, Alison M. and Tanter, \'{E}ric},
+ title = {Abstracting Gradual Typing},
+ booktitle = popl,
+ year={2016}
+}
+@article{pitts96,
+title = "Relational Properties of Domains",
+journal = "Information and Computation",
+volume = "127",
+number = "2",
+pages = "66 - 90",
+year = "1996",
+author = "Andrew M. Pitts",
+}
+
+@article{smythplotkin,
+ title={The category-theoretic solution of recursive domain equations},
+ author={Smyth, Michael B and Plotkin, Gordon D},
+ journal={SIAM Journal on Computing},
+ volume={11},
+ number={4},
+ year={1982},
+}
+
+@inproceedings{refined,
+ author={Jeremy Siek and Micahel Vitousek and Matteo Cimini and John Tang Boyland},
+ title={Refined Criteria for Gradual Typing},
+ booktitle = "1st Summit on Advances in Programming Languages",
+ series={SNAPL 2015},
+ year={2015},
+}
+@inproceedings{gradualizer16,
+ author = {Cimini, Matteo and Siek, Jeremy G.},
+ title = {The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems},
+ booktitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ series = {POPL '16},
+ year={2016}
+}
+@inproceedings{gradualizer17,
+ author = {Cimini, Matteo and Siek, Jeremy G.},
+ title = {Automatically Generating the Dynamic Semantics of Gradually Typed Languages},
+ booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
+ series = {POPL 2017},
+ year = {2017},
+ pages = {789--803},
+}
+
+@inproceedings{gradeffects2014,
+ author = {Ba\~{n}ados Schwerter, Felipe and Garcia, Ronald and Tanter, \'{E}ric},
+ title = {A Theory of Gradual Effect Systems},
+ booktitle = {Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming},
+ series = {ICFP '14},
+ location = {Gothenburg, Sweden},
+ pages = {283--295},
+ year={2014}
+}
+
+@inproceedings{disney2011gradual,
+ title={Gradual information flow typing},
+ author={Disney, Tim and Flanagan, Cormac},
+ booktitle={International Workshop on Scripts to Programs 2011},
+ year={2011}
+}
+
+@inproceedings{ahmed17,
+author = {Amal Ahmed and Dustin Jamner and Jeremy G. Siek and Philip Wadler},
+title = {Theorems for Free for Free: Parametricity, With and Without Types},
+booktitle = icfp,
+year = {2017},
+}
+@inproceedings{igarashipoly17,
+author = {Yuu Igarashi and Taro Sekiyama and Atsushi Igarashi},
+title = {On Polymorphic Gradual Typing},
+booktitle = icfp17,
+year = {2017},
+}
+@inproceedings{igarashisession17,
+author = {Atsushi Igarashi and Peter Thiemann and Vasco Vasconcelos and Philip Wadler},
+title = {Gradual Session Types},
+booktitle = icfp,
+year = {2017},
+}
+@Inbook{freyd91,
+author="Freyd, Peter",
+editor="Carboni, Aurelio and Pedicchio, Maria Cristina and Rosolini, Guiseppe",
+title="Algebraically complete categories",
+bookTitle="Category Theory: Proceedings of the International Conference held in Como, Italy, July 22--28, 1990",
+year="1991",
+pages="95--104",
+}
+@inproceedings{siek-taha07,
+ author = "Jeremy G. Siek and Walid Taha",
+ title = "Gradual Typing for Objects",
+ booktitle = ecoop,
+ year = 2007,
+}
+@article{plotkin1993logic,
+ title={A logic for parametric polymorphism},
+ author={Plotkin, Gordon and Abadi, Mart{\'\i}n},
+ journal={Typed Lambda Calculi and Applications},
+ pages={361--375},
+ year={1993},
+}
+@inproceedings{lehmann17,
+ author = {Lehmann, Nico and Tanter, \'{E}ric},
+ title = {Gradual Refinement Types},
+ booktitle = popl,
+ year={2017},
+}
+@article{felleisen-hieb,
+ author = "Matthias Felleisen and Robert Hieb",
+ title = "A Revised Report on the Syntactic Theories of Sequential Control and State",
+ journal = "Theor. Comput. Sci.",
+ volume = "103",
+ number = "2",
+ pages = "235--271",
+ year = "1992",
+}
+@article{kock95,
+title = "Monads for which structures are adjoint to units",
+journal = "Journal of Pure and Applied Algebra",
+volume = "104",
+number = "1",
+pages = "41 - 59",
+year = "1995",
+author = "Anders Kock",
+}
+
+@inproceedings{dagand16,
+ author = {Dagand, Pierre-Evariste and Tabareau, Nicolas and Tanter, \'{E}ric},
+ title = {Partial Type Equivalences for Verified Dependent Interoperability},
+ booktitle = icfp,
+ year = {2016},
+ location = {Nara, Japan},
+}
+
+@book{Lambek:1986,
+ author = {Lambek, J. and Scott, P. J.},
+ title = {Introduction to Higher Order Categorical Logic},
+ year = {1986},
+ isbn = {0-521-24665-2},
+ publisher = {Cambridge University Press},
+}
+
+@article{crutwell-shulman,
+Author = {G. S. H. Cruttwell and Michael A. Shulman},
+Title = {A unified framework for generalized multicategories},
+Year = {2009},
+Eprint = {arXiv:0907.2460},
+journal = {Theory and Applications of Categories},
+volume = {24},
+number = {21}
+}
+
+@article{wand79ocat,
+title = "Fixed-point constructions in order-enriched categories",
+journal = "Theoretical Computer Science",
+volume = "8",
+number = "1",
+pages = "13 - 30",
+year = "1979",
+note = "",
+author = "Mitchell Wand"
+}
+
+@phdthesis{Dunphy:2002,
+ author = {Dunphy, Brian Patrick},
+ advisor = {Reddy, Uday},
+ title = {Parametricity As a Notion of Uniformity in Reflexive Graphs},
+ year = {2002},
+ isbn = {0-493-89955-3},
+ publisher = {University of Illinois at Urbana-Champaign},
+ address = {Champaign, IL, USA},
+}
+
+@article{ohearn95,
+author = "O'Hearn, Peter W. and Tennent, Robert D.",
+title = "Parametricity and Local Variables",
+journal = jacm,
+volume = "42",
+number = "3",
+pages = "658--709",
+month = "May",
+year = "1995"}
+
+@InProceedings{johann15bifibrational,
+ title = {Bifibrational Functorial Semantics for Parametric Polymorphism},
+ author = {Neil Ghani and Patricia Johann and Fredrik Nordvall Forsberg and Federico Orsanigo and Tim Revell},
+ booktitle = { Proceedings of Mathematical Foundations of Program Semantics},
+ year = {2015}
+}
+
+@book{constable+86nuprl-book,
+ author = "Robert L. Constable and Stuart F. Allen and H. M. Bromley and
+ W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and
+ T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and
+ Scott F. Smith",
+ title="Implementing Mathematics with the {NuPRL} Proof Development System",
+ publisher={Prentice Hall},
+ year=1986
+}
+
+@unpublished{dagand:hal-01629909,
+ TITLE = {{Foundations of Dependent Interoperability}},
+ AUTHOR = {Dagand, Pierre-Evariste and Tabareau, Nicolas and Tanter, {\'E}ric},
+ URL = {https://hal.inria.fr/hal-01629909},
+ NOTE = {working paper or preprint},
+ YEAR = {2017},
+}
+
+@inproceedings{statonlevy13,
+ author = {Staton, Sam and Levy, Paul Blain},
+ title = {Universal Properties of Impure Programming Languages},
+ booktitle = popl,
+ year = 2013
+}
+
+@inproceedings{seely1984locally,
+ title={Locally cartesian closed categories and type theory},
+ author={Seely, Robert AG},
+ booktitle={Mathematical proceedings of the Cambridge philosophical society},
+ volume={95},
+ number={1},
+ pages={33--48},
+ year={1984},
+ organization={Cambridge University Press}
+}
+
+@inproceedings{hofmann1994interpretation,
+ title={On the interpretation of type theory in locally cartesian closed categories},
+ author={Hofmann, Martin},
+ booktitle={International Workshop on Computer Science Logic},
+ pages={427--441},
+ year={1994},
+}
+
+@article{clairambault2014biequivalence,
+ title={The biequivalence of locally cartesian closed categories and Martin-L{\"o}f type theories},
+ author={Clairambault, Pierre and Dybjer, Peter},
+ journal={Mathematical Structures in Computer Science},
+ volume={24},
+ number={6},
+ year={2014},
+ publisher={Cambridge University Press}
+}
+
+@article{Vakarthesis,
+ author = {Matthijs V{\'{a}}k{\'{a}}r},
+ title = {In Search of Effectful Dependent Types},
+ journal = {CoRR},
+ year = {2017},
+ url = {http://arxiv.org/abs/1706.07997},
+}
+
+@inbook{ahmanghaniplotkin16,
+ title = "Dependent Types and Fibred Computational Effects",
+ author = "Daniel Ahman and Neil Ghani and Plotkin, {Gordon D.}",
+ year = "2016",
+ doi = "10.1007/978-3-662-49630-5_3",
+ booktitle = "Foundations of Software Science and Computation Structures",
+}
+@inproceedings{ahmed08:paramseal,
+title = "Parametric polymorphism through run-time sealing, or, Theorems for low, low prices!",
+author = "Jacob Matthews and Amal Ahmed",
+booktitle = esop,
+year = 2008,
+month = mar,
+location = "Budapest, Hungary",
+}
+@phdthesis{levy01:phd,
+author = "Levy, Paul Blain",
+title = "Call-by-Push-Value",
+type = "{Ph.~D.} Dissertation",
+school = "Queen Mary, University of London",
+department = "Department of Computer Science",
+address = "London, UK",
+month = mar,
+year = "2001"}
+
+@inproceedings{neis09,
+ author = {Georg Neis and Derek Dreyer and Andreas Rossberg},
+ title = {Non-Parametric Parametricity},
+ booktitle = icfp,
+ pages = "135--148",
+ year = {2009},
+ month = sep
+}
+
+@Article{moggi91,
+ author = {Eugenio Moggi},
+ title = {Notions of computation and monads},
+ journal = {Inform. And Computation},
+ year = {1991},
+ volume = {93},
+ number = {1},
+}
+ @inproceedings{Wolff:2011:GT,
+ author = {Wolff, Roger and Garcia, Ronald and Tanter, \'{E}ric and Aldrich, Jonathan},
+ title = {Gradual Typestate},
+ booktitle = {Proceedings of the 25th European Conference on Object-oriented Programming},
+ series = {ECOOP'11},
+ year = {2011},
+}
+
+@article{extended,
+ author = {Max S. New and
+ Daniel R. Licata},
+ title = {Call-by-name Gradual Type Theory},
+ journal = {CoRR},
+ year = {2018},
+ url = {http://arxiv.org/abs/1802.00061},
+}
+
+@article{newlicata2018-fscd,
+ author = {Max S. New and
+ Daniel R. Licata},
+ title = {Call-by-name Gradual Type Theory},
+ journal = {FSCD},
+ year = {2018},
+}
+
+@article{martinlof83sienna,
+ year = {1983/1996},
+ journal = {Nordic Journal of Philosophical Logic},
+ publisher = {Scandinavian University Press},
+ volume = {1},
+ author = {Per Martin{-}L\"of},
+ number = {1},
+ title = {On the Meanings of the Logical Constants and the Justifications of the Logical Laws (Sienna Lectures)},
+ pages = {11--60}
+}
+
+@Article{pfenningdavies,
+ author = {Frank Pfenning and Rowan Davies},
+ title = {A Judgmental Reconstruction of Modal Logic},
+ journal = {Mathematical Structures in Computer Science},
+ year = {2001},
+ volume = {11},
+ pages = {511-540},
+}
+
+@article{dagand18,
+ title={Foundations of dependent interoperability},
+ volume={28},
+ DOI={10.1017/S0956796818000011},
+ journal={Journal of Functional Programming},
+ publisher={Cambridge University Press},
+ author={Dagand, Pierr-\'{E}variste and Tabareau, Nicolas and Tanter, \'{E}ric},
+ year={2018},
+ pages={e9}
+}
+
+@inproceedings{thatte90,
+ author = "Satish Thatte",
+ title = "Quasi-static typing",
+ booktitle = popl,
+ pages = "367--381",
+ year = 1990
+}
+
+@misc{hejlsberg12,
+ Author = {Anders Hejlsberg},
+ Date-Added = {2014-01-06 15:39:32 +0000},
+ Date-Modified = {2014-09-11 10:40:22 +0000},
+ Howpublished = {Microsoft Channel 9 Blog},
+ Title = {Introducing {TypeScript}},
+ Year = {2012}}
+
+@incollection{bierman14,
+ Author = {Bierman, Gavin and Abadi, Mart{\'\i}n and Torgersen, Mads},
+ Booktitle = {ECOOP 2014 -- Object-Oriented Programming},
+ Date-Added = {2014-10-06 15:02:06 +0000},
+ Date-Modified = {2015-11-06 03:05:46 +0000},
+ Editor = {Jones, Richard},
+ Language = {English},
+ Pages = {257-281},
+ Publisher = {Springer Berlin Heidelberg},
+ Series = {Lecture Notes in Computer Science},
+ Title = {Understanding {TypeScript}},
+ Volume = {8586},
+ Year = {2014}}
+
+@inproceedings{verlaguet13,
+ Author = {Julien Verlaguet},
+ Booktitle = {Commercial Users of Functional Programming (CUFP)},
+ Date-Added = {2014-01-06 15:28:27 +0000},
+ Date-Modified = {2014-04-14 11:23:23 +0000},
+ Title = {Facebook: Analyzing {PHP} statically},
+ Year = {2013}}
+
+@url{chaudhuri14,
+ Author = {Avik Chaudhuri},
+ Date-Added = {2015-07-16 16:32:06 +0000},
+ Date-Modified = {2015-11-18 04:29:52 +0000},
+ Keywords = {gradual typing},
+ Title = {Flow: a static type checker for JavaScript},
+ Url = {http://flowtype.org/},
+ Urldate = {2014},
+ Year = {2014},
+ Bdsk-Url-1 = {http://flowtype.org/}}
+
+@manual{bracha11,
+ Author = {Gilad Bracha},
+ Date-Added = {2014-04-14 10:26:35 +0000},
+ Date-Modified = {2014-04-14 10:27:35 +0000},
+ Month = {October},
+ Organization = {Google},
+ Title = {Optional Types in {Dart}},
+ Year = {2011}}
+
+@misc{hejlsberg10,
+ Author = {Anders Hejlsberg},
+ Date-Added = {2014-01-06 15:43:48 +0000},
+ Date-Modified = {2014-01-06 16:09:03 +0000},
+ Howpublished = {Microsoft Channel 9 Blog},
+ Month = {April},
+ Title = {C\# 4.0 and beyond by Anders Hejlsberg},
+ Year = {2010}}
+
+@Misc{turner14:typescript,
+ author = {Jonathan Turner},
+ title = {TypeScript and the Road to 2.0},
+ Url = {https://blogs.msdn.microsoft.com/typescript/2014/10/22/typescript-and-the-road-to-2-0/},
+ month = {October},
+ year = 2014}
+
+@inproceedings{siek15:mono,
+ author = {Siek, Jeremy G. and Vitousek, Michael M. and Cimini, Matteo and Tobin-Hochstadt, Sam and Garcia, Ronald},
+ title = {Monotonic References for Efficient Gradual Typing},
+ booktitle = {Proceedings of the 24th European Symposium on Programming on Programming Languages and Systems - Volume 9032},
+ year = {2015},
+}
+
+@misc{hack14:blog,
+ author = {Julien Verlaguet and Alek Menghrajani},
+ title = {Hack: a new programming language for HHVM},
+ url = {https://code.facebook.com/posts/264544830379293/hack-a-new-programming-language-for-hhvm/},
+ month = {March},
+ year = {2014}
+}
+
+@inproceedings{gronski06,
+ author = "Jessica Gronski and Kenneth Knowles and Aaron Tomb and Stephen N. Freund and Cormac Flanagan",
+ title = "Sage: Hybrid Checking for Flexible Specifications",
+ booktitle = scheme,
+ month = sep,
+ pages = "93--104",
+ year = 2006
+}
+
+@inproceedings{Ina:2011zr,
+ Author = {Ina, Lintaro and Igarashi, Atsushi},
+ Booktitle = {Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications},
+ Date-Added = {2012-11-09 23:27:38 +0000},
+ Date-Modified = {2012-12-20 08:58:22 -0700},
+ Keywords = {dynamic types, generics, gradual typing},
+ Series = {OOPSLA '11},
+ Title = {Gradual typing for generics},
+ Year = {2011}}
+
+@inproceedings{swamy14,
+author = {Nikhil Swamy and C{\'e}dric Fournet and Aseem Rastogi and
+ Karthikeyan Bhargavan and Juan Chen and Pierre-Yves Strub and Gavin M. Bierman},
+title = {Gradual typing embedded securely in {J}ava{S}cript},
+booktitle = popl14,
+year = {2014},
+pages = {425-438}
+}
+
+@article{Allende:2013aa,
+ Author = {Esteban Allende and Oscar Calla{\'u} and Johan Fabry and {\'E}ric Tanter and Marcus Denker},
+ Date-Added = {2014-03-29 03:55:17 +0000},
+ Date-Modified = {2014-03-29 03:55:20 +0000},
+ Journal = {Science of Computer Programming},
+ Month = aug,
+ Note = {Available online},
+ Publisher = {Elsevier},
+ Title = {Gradual Typing for {Smalltalk}},
+ Urldoi = {http://dx.doi.org/10.1016/j.scico.2013.06.006},
+ Urlpdf = {http://pleiad.dcc.uchile.cl/papers/2013/allendeAl-scp2013.pdf},
+ Users = {eallende , ocallau , jfabry , etanter},
+ Year = 2013}
+
+@inproceedings{ahmed06:lr,
+title = "Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types",
+author = "Amal Ahmed",
+booktitle = esop,
+year = 2006,
+month = mar,
+location = "Vienna, Austria",
+pages = "69--83"}
+
+@techreport{ahmed06:esop06-techrpt,
+author = "Amal Ahmed",
+title = "Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types",
+institution = "Harvard University",
+number = "TR-01-06",
+month = jan,
+year = 2006,
+note="Available at \texttt{http://www.cs.indiana.edu/\linebreak[0]$\sim$amal/\linebreak[0]papers/\linebreak[0]lr-recquant-techrpt.pdf}"}
+
+@article{fuhrmann1999direct,
+ title={Direct models of the computational lambda-calculus},
+ author={F{\"u}hrmann, Carsten},
+ journal={Electronic Notes in Theoretical Computer Science},
+ volume={20},
+ pages={245--292},
+ year={1999},
+}