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> 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> 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> 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> shows that the definitions given there
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
an upcast $A \ltdyn A'$ and a downcast $\defdncast{\u F A}{\u F A'}$.
We need a
downcast $\defdncast{\u F A}{F A'}$, which we have,
and an upcast $\defdncast{U \u F A}{U \u F A'}$, which is
constructed as in Theorem <ref>.

As discussed in Section <ref>, rather than an upcast being
a complex value $x : A \vdash \upcast{A}{A'}{x} : A'$, an a priori more
general type would be a stack $\bullet : \u F A \vdash \upcast{\u F
A}{\u F A'}{\bullet} : \u F A'$, which allows the upcast to perform
effects; dually, an a priori more general type for a downcast $\bullet :
\u B' \vdash \dncast{\u B}{\u B'}{\bullet} : \u B$ would be a value $x :
U \u B' \vdash \dncast{U \u B}{U \u B'}{x} : U \u B$, which allows the
downcast to ignore its argument.  The following shows that in GTT$_G$,
if we postulate such stack upcasts/value downcasts as originally
suggested in Section <ref>, then in fact these casts
must be equal to the action of $U$/$\u F$ on some
value upcasts/stack downcasts, so the potential
for (co)effectfulness affords no additional flexibility.

Suppose we extend GTT$_G$ with the following postulated stack upcasts
and value downcasts (in the sense of
Definition <ref>): For every type
precision $A \ltdyn A'$, there is a stack upcast $\bullet : \u F A
\vdash \upcast{\u F A}{\u F A'}{\bullet} : \u F A'$, and for every $\u
B \ltdyn \u B'$, there is a complex value downcast $x : U \u B' \vdash
\dncast{U \u B}{U \u B'}{x} : 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}
\bullet : \u F A \vdash \upcast{\u F A}{\u F A'}{\bullet} \equidyn { (\bindXtoYinZ{{\bullet}}{x:A}{\ret{(\defupcast{A}{A'}{x})}})}\\
x : U \u B' \vdash \dncast{U \u B}{U \u B'}{x} \equidyn {(\thunk{(\defdncast{\u B}{\u B'}{(\force x)})})}
\end{array}
\]

Lemma <ref> constructs $\defupcast{A}{A'}$ and
$\defdncast{\u B}{\u B'}$, so the proof of
Theorem <ref> (which really works for any
$\defupcast{A}{A'}$ and $\defdncast{\u B}{\u B'}$ with the correct
universal properties, not only the postulated casts) implies that the
right-hand sides of the above equations are stack upcasts and value
downcasts of the appropriate type.  Since stack upcasts/value downcasts
are unique by an argument analogous to Theorem <ref>,
the postulated casts must be equal to these.

Indeed, the following a priori even more general assumption provides no
more flexibility:

Suppose we extend GTT$_G$ only with postulated monadic upcasts $x : U
\u F A \vdash \upcast{U \u F A}{U \u F A'}{x} : U \u F A'$ for every
$A \ltdyn A'$ and comonadic downcasts $\bullet : \u F U \u B' \vdash
\dncast{\u F U \u B}{\u F U \u B'}{\bullet} : \u F U \u B$ for every
$\u B \ltdyn \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}
\]

In CBV terms, the monadic upcast is like an upcast from $A$ to $A'$
taking having type $(1 \to A) \to A'$, i.e. it takes a thunked
effectful computation of an $A$ as input and produces an effectful
computation of an $A'$.

Again, Lemma <ref> constructs $\defupcast{A}{A'}$
and $\defdncast{\u B}{\u B'}$, so the proof of part (5) of
Theorem <ref> gives the result.

§.§ Equidynamic Types are Isomorphic

* If $A \ltdyn A'$ and $A' \ltdyn A$ then $A \cong_v A'$.

* If $\u B \ltdyn \u B'$ and $\u B' \ltdyn \u B$ then $\u B \cong_c \u B'$.

* We have upcasts $x : A \vdash \upcast{A}{A'}{x} : A'$ and $x' : A' \vdash \upcast{A'}{A}{x'} : A$.
For the composites, to show
$x : A \vdash \upcast{A'}{A}{\upcast{A}{A'}{x}} \ltdyn x$
we apply upcast left twice, and conclude $x \ltdyn x$ by assumption.
To show,
$x : A \vdash x \ltdyn \upcast{A'}{A}{\upcast{A}{A'}{x}}$,
we have $x : A \vdash x \ltdyn {\upcast{A}{A'}{x}} : A \ltdyn A'$
by upcast right, and therefore
$x : A \vdash x \ltdyn \upcast{A'}{A}{\upcast{A}{A'}{x}} : A \ltdyn A$
again by upcast right.
The other composite is the same proof with $A$ and $A'$ swapped.

* We have downcasts $\bullet : \u B \vdash \dncast{\u B}{\u B'}{\bullet} : \u B'$ and
$\bullet : \u B' \vdash \dncast{\u B'}{\u B}{\bullet} : \u B$.

For the composites, to show $\bullet : \u B' \vdash \bullet \ltdyn
\dncast{\u B'}{\u B}{\dncast{\u B}{\u B'}}{\bullet}$, we apply
downcast right twice, and conclude $\bullet \ltdyn \bullet$.  For
$\dncast{\u B'}{\u B}{\dncast{\u B}{\u B'}}{\bullet} \ltdyn
\bullet$, we first have $\dncast{\u B}{\u B'}{\bullet} \ltdyn
\bullet : \u B \ltdyn \u B'$ by downcast left, and then the result
by another application of downcast left.
The other composite is the same proof with $\u B$ and $\u B'$ swapped.

§ CONTRACT MODELS OF GTT

To show the soundness of our theory, and demonstrate its relationship to
operational definitions of observational equivalence and the gradual
guarantee, we develop models of GTT using observational error
approximation of a non-gradual CBPV.

We call this the contract translation because it translates the
built-in casts of the gradual language into ordinary terms implemented
in a non-gradual language.

While contracts are typically implemented in a dynamically typed
language, our target is typed, retaining type information similarly to
manifest contracts <cit.>.

We give implementations of the dynamic value type in the usual way as
a recursive sum of basic value types, i.e., using type tags, and we
give implementations of the dynamic computation type as the dual: a
recursive product of basic computation types.

Writing $\sem{M}$ for any of the contract translations, the remaining
sections of the paper establish:

If $\Gamma \vdash M_1 \equidyn M_2 : \u B$, then for any closing
GTT context $C : (\Gamma \vdash \u B) \Rightarrow (\cdot \vdash \u F
(1+1))$, $\sem{C[M_1]}$ and $\sem{C[M_2]}$ have the same behavior: both diverge,
both run to an error, or both run to $\tru$ or both run to $\fls$.

If $\Gamma_1 \ltdyn \Gamma_2 \vdash M_1 \ltdyn M_2 : B_1 \ltdyn B_2$,
then for any GTT context $C : (\Gamma_1 \vdash B_1) \Rightarrow (\cdot
\vdash \u F (1+1))$, and any valid interpretation of the dynamic
types, either

* $\sem{C[M_1]} \Downarrow \err$, or

* $\sem{C[M_1]} \Uparrow$ and $\sem{C[\dncast{B_1}{B_2}M_2[\upcast{\Gamma_1}{\Gamma_2}{\Gamma_1}]]} \Uparrow$, or

* $\sem{C[M_1]} \Downarrow \ret V$,
\Downarrow \ret V$, and $V = \tru$ or $V = \fls$.

As a consequence we will also get consistency of our logic of

$\cdot \vdash \ret \kw{true} \ltdyn \ret \kw{false} : \u F(1+1)$ is not
provable in GTT.

They are distinguished by the identity context.

We break down this proof into 3 major steps.

* (This section) We translate GTT into a statically typed
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.
Our translation is parameterized by the implementation of the dynamic
types, and we demonstrate two valid implementations, one more direct
and one more Scheme-like.

* (Section <ref>) Next, we eliminate all uses of complex
values and stacks from the CBPV language. We translate the complex
values and stacks to terms with a proof that they are “pure”
(thunkable or linear <cit.>). This part has little to do with GTT
specifically, except that it shows the behavioral property that
corresponds to upcasts being complex values and downcasts being
complex stacks.

* (Section <ref>) Finally, with complex values and stacks
eliminated, we give a standard operational semantics for CBPV and
define a logical relation that is sound and complete with
respect to observational error approximation. Using the logical
relation, we show that the inequational theory of CBPV is sound for
observational error approximation.

By composing these, we get a model of GTT where equidynamism is sound
for observational equivalence and an operational semantics that
satisfies the graduality theorem.

§.§ Call-by-push-value

Next, we define the call-by-push-value language  that will be
the target for our contract translations of GTT.

is the axiomatic version of call-by-push-value with
complex values and stacks, while  (Section <ref>) will
designate the operational version of call-by-push-value with only
operational values and stacks.

is almost a subset of GTT obtained as follows: We remove the
casts and the dynamic types $\dynv, \dync$ (the shaded pieces) from the
syntax and typing rules in Figure <ref>.  There
is no type dynamism, and the inequational theory of * is the
homogeneous fragment of term dynamism in
Figure <ref> and Figure <ref> (judgements $\Gamma \vdash
E \ltdyn E' : T$ where $\Gamma \vdash E,E' : T$, with all the same rules
in that figure thus restricted).  The inequational axioms are the
Type Universal Properties ($\beta\eta$ rules)
and Error Properties (with ErrBot made homogeneous) from
Figure <ref>.

To implement the casts and dynamic types, we add general
recursive value types ($\mu X.A$, the fixed point of $X \vtype
\vdash A \vtype$) and corecursive computation types ($\nu \u Y.\u
B$, the fixed point of $\u Y \ctype \vdash \u B \ctype$).

The recursive type $\mu X.A$ is a value type with constructor
$\texttt{roll}$, whose eliminator is pattern matching, whereas the
corecursive type $\nu \u Y.\u B$ is a computation type defined by its
eliminator (), with an introduction form that we also write
as .

We extend the inequational theory with monotonicity of each term constructor of
the recursive types, and with their $\beta\eta$ rules.

The rules for recursive types are in the extended version.

In the following figure, we write $\bnfadd$ and $\bnfsub$ to indicate
the diff from the grammar in Figure <ref>.

\[
\begin{array}{lrcl}
\text{Value Types} & A & \bnfadd & \mu X. A \alt X\\
&   & \bnfsub & \dynv \\
\text{Computation Types} & \u B & \bnfadd & \nu \u Y. \u B \alt \u Y\\
&      & \bnfsub & \dync\\
\text{Values} & V & \bnfadd & \rollty{\mu X.A} V\\
&   & \bnfsub & \upcast{A}{A} V\\
\text{Terms} & M & \bnfadd & \rollty{\nu \u Y. \u B} M \alt \unroll M\\
& M & \bnfsub & \dncast{\u B}{\u B}M\\
\text{Both}  & E & \bnfadd & \pmmuXtoYinZ V x E
\end{array}
\]

Γ⊢V : A[μX. A/X]
Γ⊢μX. A V : μX.A
Γ⊢V : μX. A

Γ, x : A[μX.A/X] Δ⊢E : T

ΓΔ⊢V x E : T

Γ|Δ⊢M : B̆[νY̆. B̆]
Γ|Δ⊢νY̆. B̆ M : νY̆. B̆

Γ|Δ⊢M : νY̆. B̆
Γ|Δ⊢M : B̆[νY̆. B̆]

Γ⊢V V' : A[μX. A/X]
Γ⊢V V' : μX. A

Γ⊢V V' : μX.AΓ, x : A[μX. A/X] Δ⊢E E' : T
ΓΔ⊢V x E V' x E' : T

ΓΔ⊢M M' : B̆[νY̆. B̆/Y̆]
ΓΔ⊢M M' : νY̆. B̆

ΓΔ⊢M M' : νY̆. B̆
ΓΔ⊢M M' : B̆[νY̆. B̆/Y̆]

Recursive Type Axioms

Type     $\beta$     $\eta$

${\pmmuXtoYinZ{\roll V}{x}{E} \equidyn E[V/x]}$

E \equidyn \pmmuXtoYinZ x {y} E[\roll y/x] \\
\text{where } {x : \mu X. A \vdash E : T}
\end{array}$

${\unroll\roll M \equidyn M}$

${\bullet : \nu \u Y. \u B \vdash \bullet \equidyn \roll\unroll \bullet : \nu \u Y. \u B}$

types, terms, recursive types (diff from GTT),
full rules in the extended version

§.§ Interpreting the Dynamic Types

As shown in Theorems <ref>,
<ref>, <ref>, almost
all of the contract translation is uniquely determined already.

However, the interpretation of the dynamic types and the casts between
the dynamic types and ground types $G$ and $\u G$ are not determined
(they were still postulated in Lemma <ref>).

For this reason, our translation is parameterized by an
interpretation of the dynamic types and the ground casts.

By Theorems <ref>, <ref>, we know
that these must be embedding-projection pairs (ep pairs), which
we now define in .

There are two kinds of ep pairs we consider: those between value types
(where the embedding models an upcast) and those between computation
types (where the projection models a downcast).

* A value ep pair from $A$ to $A'$ consists of
an embedding value $x:A\vdash V_e : A'$
and projection stack $\bullet : \u F A' \vdash S_p : \u F A$,
satisfying the retraction and projection properties:

\[
x : A \vdash \ret x \equidyn S_p[\ret V_e] : \u F A
\qquad
\bullet : \u F A' \vdash \bindXtoYinZ {S_p} x \ret V_e \ltdyn \bullet : \u F A'
\]

* A computation ep pair from $\u B$ to $\u B'$ consists of
an embedding value $z : U \u B \vdash V_e : U \u B'$
and a projection stack $\bullet : \u B' \vdash S_p : \u B$
satisfying retraction and projection properties:

\[
z : U \u B \vdash \force z \equidyn S_p[\force V_e] : \u B
\qquad
w : U \u B' \vdash V_e[\thunk {S_p[\force w]}] \ltdyn w : U \u B'
\]

While this formulation is very convenient in that both kinds of ep
pairs are pairs of a value and a stack, the projection properties are
often occur more naturally in the following forms:

If $(V_e,S_p)$ is a value ep pair from $A$ to $A'$ and $\Gamma,
y:A'\pipe\Delta \vdash M : \u B$, then

\[ \Gamma , x' : A' \vdash \bindXtoYinZ {S_p[\ret x']} x M[V_e/y] \ltdyn M[x'/y] \]

Similarly, if $(V_e,S_p)$ is a computation ep pair from $\u B$ to
$\u B'$, and $\Gamma \vdash M : \u B'$then

\[ \Gamma \vdash V_e[\thunk S_p[M]] \ltdyn \thunk M : U \u B' \]

For the first,

\begin{align*}
\bindXtoYinZ {S_p[\ret x']} x M[V_e/y]
& \equidyn
\bindXtoYinZ {(\bindXtoYinZ {S_p[\ret x']} x \ret V_e)} y M\tag{comm conv, $\u F \beta$}\\
&\bindXtoYinZ {\ret x'} y M\tag{projection}\\
&M[x'/y]\tag{$\u F\beta$}
\end{align*}

For the second,

\begin{align*}
V_e[\thunk S_p[M]]
&\equidyn V_e[\thunk S_p[\force\thunk M]] \tag{$U\beta$}\\
&\ltdyn \thunk M\tag{projection}
\end{align*}

Using this, and using the notion of ground type from
Section <ref> with $0$ and $\top$ removed, we define

A $\dynv,\dync$ interpretation $\rho$ consists of (1) a
value type $\rho(\dynv)$, (2) a  computation
type $\rho(\dync)$,
for each value ground type $G$,
a value ep pair $(x.\rho_{e}(G), \rho_{p}(G))$ from $\srho G$ to
$\rho(\dynv)$, and (4) for each computation ground type $\u G$, a
computation ep pair $(z.\rho_{e}(\u G), \rho_{p}(\u G))$ from
$\srho{\u G}$ to $\rho(\dync)$.  We write
$\srho G$ and $\srho {\u G}$ for the interpretation of a ground type,
replacing $\dynv$ with $\rho(\dynv)$, $\dync$ with $\rho(\dync)$, and
compositionally otherwise.

Next, we show several possible interpretations of the dynamic type
that will all give, by construction, implementations that satisfy the
gradual guarantee.

Our interpretations of the value dynamic type are not surprising.

They are the usual construction of the dynamic type using type tags:
i.e., a recursive sum of basic value types.

On the other hand, our interpretations of the computation dynamic type
are less familiar.

In duality with the interpretation of $\dynv$, we interpret $\dync$ as
a recursive product of basic computation types.

This interpretation has some analogues in previous work on the duality
of computation <cit.>, but the
most direct interpretation (definition <ref>)
does not correspond to any known work on dynamic/gradual typing.

Then we show that a particular choice of which computation types is
basic and which are derived produces an interpretation of the dynamic
computation type as a type of variable-arity functions whose arguments
are passed on the stack, producing a model similar to Scheme without
accounting for control effects (definition

§.§.§ Natural Dynamic Type Interpretation

Our first dynamic type interpretation is to make the value and
computation dynamic types sums and products of the ground value and
computation types, respectively.

This forms a model of GTT for the following reasons.

For the value dynamic type $\dynv$, we need a value embedding (the
upcast) from each ground value type $G$ with a corresponding projection.

The easiest way to do this would be if for each $G$, we could rewrite
$\dynv$ as a sum of the values that fit $G$ and those that don't:
$\dynv \cong G + \dynv_{-G}$ because of the following lemma.

For any $A, A'$, there are value ep pairs from $A$ and $A'$ to
$A+A'$ where the embeddings are $\inl$ and $\inr$.

Define the embedding of $A$ to just be $x. \inl x$ and the
projection to be $\bindXtoYinZ \bullet y \caseofXthenYelseZ y {\inl x. \ret
x}{\inr _. \err}$.

This satisfies retraction (using $\u F(+)$ induction (lemma <ref>), $\inr$ case is the same):

\begin{align*}
\bindXtoYinZ {\inl x} y \caseofXthenYelseZ y {\inl x. \ret x}{\inr _. \err}
&\equidyn \caseofXthenYelseZ {\inl x} {\inl x. \ret x}{\inr _. \err}\tag{$\u F\beta$}\\
&\equidyn \ret x\tag{$+\beta$}
\end{align*}

and projection (similarly using $\u F(+)$ induction):

\begin{align*}
x': A+A'
&\vdash \bindXtoYinZ x {(\bindXtoYinZ {\ret x'} y \caseofXthenYelseZ y {\inl x. \ret x}{\inr _. \err})} \ret \inl x\\
&\equidyn \bindXtoYinZ x {(\caseofXthenYelseZ {x'} {\inl x. \ret x}{\inr _. \err})}\ret \inl x\tag{$\u F\beta$}\\
&\equidyn {(\caseofXthenYelseZ {x'} {\inl x. \bindXtoYinZ {\ret x} x \ret\inl x}{\inr _. \bindXtoYinZ \err x \ret\inl x})}\tag{commuting conversion}\\
&\equidyn {(\caseofXthenYelseZ {x'} {\inl x. \ret\inl x}{\inr _. \err})}\tag{$\u F\beta,\err$ strictness}\\
&\ltdyn {(\caseofXthenYelseZ {x'} {\inl x. \ret\inl x}{\inr y. \ret\inl y})}\tag{$\err$ bottom}\\
&\equidyn \ret x' \tag{$+\eta$}
\end{align*}

Whose proof relies on the following induction principle for the
returner type:

$\Gamma\pipe \cdot : \u F (A_1 + A_2) \vdash M_1 \ltdyn M_2 : \u B$
holds if and only if
$\Gamma, V_1: A_1 \vdash M_1[\ret \inl V_1] \ltdyn M_2[\ret \inl V_2] : \u B$ and
$\Gamma, V_2: A_2 \vdash M_2[\ret \inr V_2] \ltdyn M_2[\ret \inr V_2] : \u B$

This shows why the type tag interpretation works: it makes the dynamic
type in some sense the minimal type with injections from each $G$:
the sum of all value ground types $? \cong \Sigma_{G} G$.

The dynamic computation type $\dync$ can be naturally defined by a
dual construction, by the following dual argument.

First, we want a computation ep pair from $\u G$ to $\dync$ for each
ground computation type $\u G$.

Specifically, this means we want a stack from $\dync$ to $\u G$ (the
downcast) with an embedding.

The easiest way to get this is if, for each ground computation type
$\u G$, $\dync$ is equivalent to a lazy product of $\u G$ and “the
other behaviors”, i.e., $\dync \cong \u G \with \dync_{-\u G}$.

Then the embedding on $\pi$ performs the embedded computation, but on
$\pi'$ raises a type error.

The following lemma, dual to lemma <ref>
shows this forms a computation ep pair:

For any $\u B, \u B'$, there are computation ep pairs from $\u B$
and $\u B'$ to $\u B \with \u B'$ where the projections are $\pi$
and $\pi'$.

Define the projection for $\u B$ to be $\pi$. Define the embedding
by $z. \pair{\force z}{\err}$. Similarly define the projection for
$\u B'$.

This satisfies retraction:

\begin{align*}
\pi\force\thunk\pair{\force z}{\err}
&\equidyn \pi\pair{\force z}{\err}\tag{$U\beta$}\\
&\equidyn \force z\tag{$\with\beta$}
\end{align*}

and projection:

\begin{align*}
&\thunk\pair{\force\thunk\pi\force w}{\err}\\
&\equidyn \thunk\pair{\pi\force w}{\err} \tag{$U\beta$}\\
&\ltdyn \thunk\pair{\pi\force w}{\pi'\force w}\tag{$\err$ bottom}\\
&\equidyn \thunk\force w\tag{$\with\eta$}\\
&\equidyn w \tag{$U\eta$}
\end{align*}

From this, we see that the easiest way to construct an interpretation
of the dynamic computation type is to make it a lazy product of all
the ground types $\u G$: $\dync \cong \With_{\u G} \u G$.

Using recursive types, we can easily make this a definition of the

The following defines a dynamic type interpretation.

We define the types to satisfy the isomorphisms

\[
\dynv \cong 1 + (\dynv \times \dynv) + (\dynv + \dynv) + U\dync \qquad
\dync \cong (\dync \with \dync) \with (\dynv \to \dync) \with \u F \dynv
\]

with the ep pairs defined as in
Lemma <ref> and

We can construct $\dynv, \dync$ explicitly using recursive and
corecursive types. Specifically, we make the recursion explicit by
defining open versions of the types:

\begin{align*}
X,\u Y \vdash \dynv_o &= 1 + (X \times X) + (X + X) + U\u Y\vtype \\
X,\u Y \vdash \dync_o &= (\u Y \with \u Y) \with (X \to \u Y) \with \u F X \ctype
\end{align*}

Then we define the types $\dynv, \dync$ using a standard encoding:

\begin{align*}
\dynv &= \mu X. \dynv_o[\nu \u Y. \dync_o/\u Y]\\
\dync &= \nu \u Y. \dync_o[\mu X. \dynv_o/X]
\end{align*}

Then clearly by the roll/unroll isomorphism we get the desired

\begin{align*}
\dynv &\cong \dynv_o[\dync/\u Y,\dynv/X] = 1 + (\dynv \times \dynv) + (\dynv + \dynv) + U\dync \\
\dync &\cong\dynv_c[\dynv/X,\dync/\u Y] = (\dync \with \dync) \with (\dynv \to \dync) \with \u F \dynv
\end{align*}

This dynamic type interpretation is a natural fit for CBPV because the
introduction forms for $\dynv$ are exactly the introduction forms for
all of the value types (unit, pairing,$\texttt{inl}$, $\texttt{inr}$, $\texttt{force}$), while
elimination forms are all of the elimination forms for computation types
($\pi$, $\pi'$, application and binding); such “bityped” languages
are related to <cit.>.

In the extended version, we give an extension of GTT axiomatizing this
implementation of the dynamic types.

Based on this dynamic type interpretation, we can extend GTT to support
a truly dynamically typed style of programming, where one can perform
case-analysis on the dynamic types at runtime, in addition to the type
assertions provided by upcasts and downcasts.

ΓΔ⊢V :

Γ,x_1 : 1Δ⊢E_1 : T

Γ,x_×: ×Δ⊢E_×: T

Γ,x_+ : +Δ⊢E_+ : T

Γ,x_U : UΔ⊢E_U : T

ΓΔ⊢V x_1. E_1x_×. E_×x_+. E_+x_U. E_U : T

(GV) x_1. E_1x_×. E_×x_+. E_+x_U. E_U E_G[V/x_G]    (β)

Γ, x : Δ⊢E : B̆
E x
x_1. E[1/x_1]
x_×. E[×/x_×]
x_+. E[+/x_+]
x_U. E[U/x_U]*[right=$\dync$]
ΓΔ⊢M_→ : →

ΓΔ⊢M_ :

ΓΔ⊢M_F̆ : F̆
ΓΔ⊢M_M_→M_F̆ :

ĞM_M_→M_F̆ M_Ğ  (β)

∙: ⊢∙∙
F̆∙  (η)

Natural Dynamic Type Extension of GTT

The axioms we choose might seem to under-specify the dynamic type, but
because of the uniqueness of adjoints, the following are derivable.

The following are derivable in GTT with the natural dynamic type extension

F̆ 1F̆ V V x_1. x_1

F̆(×)F̆ V V x_×. x_×

F̆(+ )F̆ V V x_+. x_+

F̆ UF̆V V x_U. x_U

U()UV V

U(→)UV V

UF̆UV V

We explore this in more detail with the next dynamic type

Next, we easily see that if we want to limit GTT to just the CBV types
(i.e. the only computation types are $A \to \u F A'$), then we can
restrict the dynamic types as follows:

The following is a dynamic type interpretation for the ground types of
GTT with only function computation types:

\[
\dynv \cong 1 + (\dynv + \dynv) + (\dynv \times \dynv) + U(\dync) \qquad
\dync \cong \dynv \to \u F \dynv
\]

And finally if we restrict GTT to only CBN types (i.e., the only value
type is booleans $1+1$), we can restrict the dynamic types as follows:

The following is a dynamic type interpretation for the ground types of
GTT with only boolean value types:

\[
\dynv = (1 + 1) \qquad
\dync \cong (\dync \with \dync) \with (U\dync \to \dync)
\with \u F \dynv
\]

§.§.§ Scheme-like Dynamic Type Interpretation

The above dynamic type interpretation does not correspond to any
dynamically typed language used in practice, in part because it
includes explicit cases for the “additives”, the sum type $+$ and
lazy product 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 <cit.>.

We leave modeling this nominal structure to future work, but in
minimalist languages, such as simple dialects of Scheme and Lisp, sum
types are often encoded structurally rather than nominally by
using some fixed sum type of symbols, also called atoms.

Then a value of a sum type is modeled by a pair of a symbol (to indicate
the case) and a payload with the actual value.

We can model this by using the canonical isomorphisms

\[ \dynv + \dynv \cong ((1+1) \times \dynv) \qquad \dync \with \dync \cong (1+1) \to \dync \]

and representing sums as pairs, and lazy products as functions.

The fact that isomorphisms are ep pairs is useful for constructing the
ep pairs needed in the dynamic type interpretation.

If $x:A \vdash V' : A'$ and $x':A' \vdash V : A$ are an isomorphism in
that $V[V'/x'] \equidyn x$ and $V[V/x]\equidyn x'$, then $(x.V',
\bindXtoYinZ \bullet {x'} \ret V')$ are a value ep pair from $A$ to
$A'$.  Similarly if $\bullet : \u B \vdash S' : \u B'$ and $\bullet :
\u B' \vdash S : \u B$ are an isomorphism in that $S[S']\equiv
\bullet$ and $S'[S] \equiv \bullet$ then $(z. S'[\force z], S)$ is an
ep pair from $\u B$ to $\u B'$.

With this in mind, we remove the cases for sums and lazy pairs from the
natural dynamic types, and include some atomic type as a case of
$\dynv$—for simplicity we will just use booleans.

We also do not need a case for $1$, because we can identify it with one
of the booleans, say $\texttt{true}$.

This leads to the following definition:

We can define a dynamic type interpretation with the following type

≅(1+1) + U+ (×)≅(→) F̆

The details of constructing the two mutually recursive types from
our recursive type mechanism are in the extended version.

We construct $\dynv, \dync$ explicitly as follows.

First define $X : \vtype \vdash \texttt{Tree}[X] \vtype$ to be the
type of binary trees:

\[ \texttt{Tree} = \mu X'. X + (X' \times X') \]

Next, define $X:\vtype, \u Y: ctype \vdash \texttt{VarArg}[X,\u Y]
\ctype$ to be the type of variable-arity functions from $X$ to $\u

\[ \texttt{VarArg} = \nu \u Y'. \u Y \with (X \to \u Y') \]

Then we define an open version of $\dynv, \dync$ with respect to a
variable representing the occurrences of $\dynv$ in $\dync$:

\begin{align*}
X \vtype \vdash \dynv_o &= \texttt{Tree}[(1+1) + U \dync_o] \ctype\\
X \vtype \vdash \dync_o &= \texttt{VarArg}[\u F X/\u Y] \ctype\\
\end{align*}

Then we can define the closed versions using a recursive type:

= μX. _o= _o[]

The ep pairs for $\times, U,\u F, \to$ are clear.  To define the
rest, first note that there is an ep pair from $1+1$ to $\dynv$ by
Lemma <ref>.  Next, we can define $1$ to
be the ep pair to $1+1$ defined by the left case and
Lemma <ref>, composed with this.  The ep
pair for $\dynv + \dynv$ is defined by composing the isomorphism
(which is always an ep pair)
$(\dynv + \dynv) \cong ((1+1) \times \dynv)$ with the ep pair for
$1+1$ using the action of product types on ep pairs (proven as part of
Theorem <ref>): $(\dynv + \dynv) \cong
((1+1)\times \dynv) \,\triangleleft\, (\dynv \times \dynv) \,\triangleleft\,
\dynv$ (where we write $A \triangleleft A'$ to mean there is an ep
pair from $A$ to $A'$).  Similarly, for $\dync \with \dync$, we use
action of the function type on ep pairs (also proven as part of
Theorem <ref>): $\dync \with \dync \cong
((1+1) \to \dync) \,\triangleleft\, (\dynv \to \dync) \,\triangleleft\, \dync$

Intuitively, the above definition of $\dynv$ says that it is a binary
tree whose leaves are either booleans or closures—a simple type of
S-expressions.  On the other hand, the above definition of $\dync$
models a variable-arity function (as in Scheme), which is
called with any number of dynamically typed value arguments $\dynv$
and returns a dynamically typed result $\u F \dynv$.  To see why a
$\dync$ can be called with any number of arguments, observe that its
infinite unrolling is $\u F \dynv \with (\dynv \to \u F \dynv) \with
(\dynv \to \dynv \to \u F \dynv) \with \ldots$.  This type is
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
heap-allocated single list argument.  These two are distinguished in
Scheme and the “dot args” notation witnesses the isomorphism.

If we factor out some of the recursion to use inductive and
coinductive types, we get the following isomorphisms:

≅[(1+1) + U]≅[][F̆ ]

That is a dynamically typed value is a binary tree whose leaves are
either booleans or closures.

We think of this as a simple type of S-expressions.

A dynamically typed computation is a variable-arity function that is
called with some number of dynamically typed value arguments $\dynv$
and returns a dynamically typed result $\u F \dynv$.

This captures precisely the function type of Scheme, which allows for
variable arity functions!

What's least clear is why the type

\[
\texttt{VarArg}[X][\u Y] = \nu \u Y'. (X \to \u Y') \with \u Y
\]

Should be thought of as a type of variable arity functions.

First consider the infinite unrolling of this type:

\[
\texttt{VarArg}[X][\u Y] \simeq \u Y \with (X \to \u Y) \with (X \to X \to \u Y) \with \cdots
\]

this says that a term of type $\texttt{VarArg}[X][Y]$ offers an
infinite number of possible behaviors: it can act as a function from
$X^n \to \u Y$ for any $n$.

Similarly in Scheme, a function can be called with any number of

Finally note that this type is isomorphic to a function that takes a
cons-list of arguments:

\begin{align*}
&\u Y \with (X \to \u Y) \with (X \to X \to \u Y) \with \cdots\\
&\cong(1 \to \u Y) \with ((X \times 1) \to \u Y) \with ((X \times X \times 1) \to \u Y) \with \cdots\\
&\cong(1 + (X \times 1) + (X \times X \times 1) + \cdots) \to \u Y\\
&\cong(\mu X'. 1 + (X\times X')) \to \u Y
\end{align*}

But operationally the type $\texttt{VarArg}[\dynv][\u F\dynv]$ is a
more faithful model of Scheme implementations because all of the
arguments are passed individually on the stack, whereas the type $(\mu
X. 1 + (\dynv \times X)) \to \u F X$ is a function that takes a single
argument that is a list.

These two are distinguished in Scheme and the “dot args” notation
witnesses the isomorphism.

Based on this dynamic type interpretation we can make a “Scheme-like”
extension to GTT in Figure <ref>.

First, we add a boolean type $\bool$ with $\tru$, $\fls$ and

Next, we add in the elimination form for $\dynv$ and the introduction
form for $\dync$.

The elimination form for $\dynv$ is a typed version of Scheme's
match macro.

The introduction form for $\dync$ is a typed, CBPV version of Scheme's
case-lambda construct.

Finally, we add type dynamism rules expressing the representations of
$1$, $A + A$, and $A \times A$ in terms of booleans that were explicit
in the ep pairs used in Definition <ref>.

In the extended version of the paper, we include the appropriate term
dynamism axioms, which are straightforward syntactifications of the
properties of the dynamic type interpretation, and prove a unique
implementation theorem for the new casts.

1 A + A ×AB̆ B̆ →B̆

Γ⊢, :

Γ⊢V :

Γ⊢E_t : T

Γ⊢E_f : T
ΓΔ⊢V E_t E_f : T

E_t E_f E_tE_t E_f E_f

x : ⊢E x E[/x] E[/x]

1V A+A×AV (, V)A+A×AV (, V)

πB̆B̆→B̆M M π'B̆B̆→B̆M M

ΓΔ⊢M_→ : →

ΓΔ⊢M_F̆ : F̆
ΓΔ⊢M_→M_F̆ :

ĞM_→M_F̆ M_Ğ  (β)

∙: ⊢∙→∙
F̆∙  (η)

ΓΔ⊢V : Γ, x_:Δ⊢E_: TΓ,x_U : UΔ⊢E_U : TΓ,x_×: ×Δ⊢E_×: T
ΓΔ⊢V x_. E_x_U. E_Ux_×. E_× : T

G ∈{ , ×, U}
(GV) x_. E_x_U. E_Ux_×. E_× E_G[V/x_G]     (β)

Γ, x : Δ⊢E : B̆
E x
x_. E[/x_]
x_×. E[×/x_×]
x_U. E[U/x_U]

Scheme-like Extension to GTT

The reader may be surprised by how few axioms we need to add
to GTT for this extension: for instance we only define the upcast
from $1$ to $\bool$ and not vice-versa, and similarly the sum/lazy
pair type isomorphisms only have one cast defined when a priori
there are $4$ to be defined.

Finally for the dynamic types we define $\beta$ and $\eta$ laws
that use the ground casts as injections and projections
respectively, but we don't define the corresponding dual casts (the
ones that possibly error).

In fact all of these expected axioms can be proven from those
we have shown.

Again we see the surprising rigidity of GTT: because an $\u F$
downcast is determined by its dual value upcast (and vice-versa for
$U$ upcasts), we only need to define the upcast as long as the
downcast could be implemented already.

Because we give the dynamic types the universal property of a
sum/lazy product type respectively, we can derive the
implementations of the “checking” casts.

All of the proofs are direct from the uniqueness of adjoints

In Scheme-like GTT, we can prove

\[
\dncast{\u F1}{\u F\bool}\bullet
\equidyn
\bindXtoYinZ \bullet x \ifXthenYelseZ x {\ret()}{\err}
\]

In Scheme-like GTT, we can prove

\[
\upcast{\bool \times A}{A+A}V \equidyn \pmpairWtoXYinZ V {x}{y} \ifXthenYelseZ x {\inl y}{\inr y}
\]

and the downcasts are given by lemma <ref>.

In Scheme-like GTT, we can prove

\[
\dncast{\bool\to \u B}{\u B\with\u B}\bullet
\equidyn
\lambda x:\bool. \ifXthenYelseZ x {\pi \bullet}{\pi' \bullet}
\]

and the upcasts are given by lemma <ref>.

In Scheme-like GTT we can prove

F̆ F̆ V V x_. x_

F̆(×)F̆ V V x_×. x_×

F̆ UF̆V V x_U. x_U

U(→)UV V

UF̆UV V

Finally, we note now that all of these axioms are satisfied when
using the Scheme-like dynamic type interpretation and extending the
translation of GTT into   with the following, tediously
explicit definition:

\begin{align*}
&\sem{\bool} = 1+1\\
&\sem{\tru} =\inl()\\
&\sem{\fls} =\inr()\\
&\sem{\ifXthenYelseZ V {E_t} {E_f}} = \caseofXthenYelseZ {\sem V}{x. E_t}{x.E_f}\\
&\sem{\dyncaseofXthenBoolUPair x {x_\bool. E_\bool}{x_U. E_U}{x_\times. E_\times}}
&\quad\pmmuXtoYinZ {(x:\dynv)}  {x'} \pmmuXtoYinZ {x' : \texttt{Tree}[(1+1)+U\dync]}t \caseofX t\\
&\qquad\thenY{l. \caseofXthenYelseZ l {x_\bool. \sem{E_\bool}}{x_U. \sem{E_U}}}\\
&\qquad\elseZ{x_\times. \sem{E_\times}}\\
&\sem{\dyncocaseFunF{M_\to}{M_{\u F}}}
= \rollty{\nu \u Y. (\dynv \to \u Y)\with \u F\dynv}\pair{\sem{M_\to}}{\sem{M_{\u F}}}
\end{align*}

§.§ Contract Translation

Having defined the data parameterizing the translation, we now consider
the translation of GTT into  itself.

For the remainder of the paper, we assume that we have a fixed dynamic
type interpretation $\rho$, and all proofs and definitions work for any

x:A ⊢AA' : A'∙:B̆' ⊢B̆B̆' : B̆

x : 0 ⊢0A     =     x

∙: A ⊢F̆0F̆ A    =    ∙x

x :  ⊢     =     x

∙: F̆ ⊢F̆ F̆    =    ∙

x : G ⊢G     =     ρ_up(G)

∙: F̆ ⊢F̆ GF̆    =    ρ_dn(G)

x : A ⊢A     =     ⌊A ⌋[A⌊A ⌋/x]

∙: F̆⊢A    =    AA[A]

x : A_1 + A_2 ⊢A_1 + A_2A_1' + A_2'
=     x

x_1. A_1A_1'[x_1/x]

x_2. A_2A_2'[x_2/x]

∙: A_1 + A_2 ⊢F̆(A_1 + A_2)F̆(A_1' + A_2')
∙x' x'

x_1'. (F̆A_1F̆ A_1'x_1') x_1 x_1

x_2'. (F̆A_2F̆ A_2'x_2') x_2 x_2

x : 1 ⊢11    =    x

∙: F̆ 1 ⊢F̆1F̆1    =    x

x : A_1×A_2 ⊢A_1×A_2A_1'×A_2'    =    x x_1x_2

(A_1A_1'[x_1], A_2A_2'[x_2])

∙⊢F̆(A_1 ×A_2)F̆(A_1' ×A_2')
∙x' x' x_1'x_2'

F̆A_1F̆A_1'x_1' x_1

F̆A_2F̆A_2'x_2' x_2 (x_1,x_2)

x : UF̆ A ⊢UF̆ AU F̆ A'    =
(x y AA'[y/x])

∙: B̆ ⊢⊤B̆    =    { }

x:U⊤⊢U⊤UB̆    =

∙: ⊢    =    ∙

x:U⊢UU    =    x

∙: ⊢Ğ    =    ρ_dn(Ğ)

x:UĞ ⊢UĞU    =    ρ_up(Ğ)

∙: ⊢B̆    =    B̆B̆[B̆]

x:U⊢UB̆U   =    UB̆U[UB̆UB̆]

∙: B̆_1'B̆_2'⊢B̆_1B̆_2B̆_1'B̆_2'    =    B̆_1B̆_1'π∙

x : U(B̆_1B̆_2) ⊢U(B̆_1 B̆_2)U(B̆_1'B̆_2')

∙⊢A →B̆A' →B̆'    =    λx:A. B̆B̆'(∙  (AA'x))

f : U(A →B̆) ⊢U(A →B̆)U(A' →B̆')

F̆ AF̆A'x' x

UB̆UB̆'(f)  x'

∙: F̆UB̆' ⊢F̆UB̆F̆UB̆'
∙x' B̆B̆'x'

Cast to Contract Translation (selected cases)

§.§.§ Interpreting Casts as Contracts

The main idea of the translation is an extension of the dynamic type
interpretation to an interpretation of all casts in GTT
(Figure <ref>) as contracts in , following
the definitions in Lemma <ref>.

To verify the totality and coherence of this definition, we define (in
the extended version) a normalized version of the type dynamism rules
from Figure <ref>, which is interderivable but
has at most one derivation of $T \ltdyn T'$ for a given $T$ and $T'$.
The main idea is to restrict reflexivity to base types, and restrict
transitivity to $A \ltdyn \floor{A} \ltdyn \dynv$, where $\floor{A}$
is the ground type with the same outer connective as $A$.

Some clauses of the translation are overlapping, which we resolve by
considering them as ordered (though we will ultimately show they are

The definition is also not obviously total: we need to verify that it
covers every possible case where $A \ltdyn A'$ and $\u B \ltdyn \u

To prove totality and coherence, we could try induction on the type
dynamism relation of Figure <ref>, but it is
convenient to first give an alternative, normalized set of rules for
type dynamism that proves the same relations, which we do in
Figure <ref>.

A ∈{, 1}
A A

A ∈{, 0}
0 A

A AA ∉{0,}

B̆ B̆'
U B U B'

A_1 A_1' A_2 A_2'
A_1 + A_2 A_1' + A_2'

A_1 A_1' A_2 A_2'
A_1 ×A_2 A_1' ×A_2'

B̆ ∈{ , ⊤}

B̆ B̆ B̆ ∉{ ⊤, }

A A'
F̆ A F̆ A'

B̆_1 B̆_1' B̆_2 B̆_2'
B̆_1 B̆_2 B̆_1' B̆_2'

A A' B̆ B̆'
A →B̆ A' →B̆'

Normalized Type Dynamism Relation

$T \ltdyn T'$ is provable in the normalized typed dynamism
definition iff it is provable in the original typed
dynamism definition.

It is clear that the normalized system is a subset of the original:
every normalized rule corresponds directly to a rule of the original
system, except the normalized $A \ltdyn \dynv$ and $\u B \ltdyn \dync$
rules have a subderivation that was not present originally.

For the converse, first we show by induction that reflexivity is

* If $A \in \{\dynv, 1, 0\}$, we use a normalized rule.

* If $A \not\in\{\dynv, 1, 0\}$, we use the inductive hypothesis
and the monotonicity rule.

* If $\u B\in \{\dync, \top\}$ use the normalized rule.

* If $\u B \not\in\{\dync, \top\}$ use the inductive hypothesis
and monotonicity rule.

Next, we show that transitivity is admissible:

* Assume we have $A \ltdyn A' \ltdyn A''$

* If the left rule is $0 \ltdyn A'$, then either $A' = \dynv$
or $A' = 0$. If $A' = 0$ the right rule is $0 \ltdyn A''$ and we
can use that proof. Otherwise, $A' = \dynv$ then the right rule
is $\dynv \ltdyn \dynv$ and we can use $0 \ltdyn \dynv$.

* If the left rule is $A \ltdyn A$ where $A \in \{ \dynv, 1\}$
then either $A = \dynv$, in which case $A'' = \dynv$ and we're
done.  Otherwise the right rule is either $1 \ltdyn 1$ (done) or
$1 \ltdyn \dynv$ (also done).

* If the left rule is $A \ltdyn \dynv$ with
$A\not\in\{0,\dynv\}$ then the right rule must be $\dynv \ltdyn
\dynv$ and we're done.

* Otherwise the left rule is a monotonicity rule for one of
$U, +, \times$ and the right rule is either monotonicity (use
the inductive hypothesis) or the right rule is $A' \ltdyn \dynv$
with a sub-proof of $A' \ltdyn \floor{A'}$. Since the left rule
is monotonicity, $\floor{A} = \floor{A'}$, so we inductively use
transitivity of the proof of $A \ltdyn A'$ with the proof of $A'
\ltdyn \floor{A'}$ to get a proof $A \ltdyn \floor{A}$ and thus
$A \ltdyn \dynv$.

* Assume we have $\u B \ltdyn \u B' \ltdyn \u B''$.

* If the left rule is $\top \ltdyn \u B'$ then $\u B'' \in
\{\dync, \top\}$ so we apply that rule.

* If the left rule is $\dync\ltdyn \dync$, the right rule must
be as well.

* If the left rule is $\u B \ltdyn \dync$ the right rule must
be reflexivity.

* If the left rule is a monotonicity rule for $\with, \to, \u
F$ then the right rule is either also monotonicity (use the
inductive hypothesis) or it's a $\u B \ltdyn \dync$ rule and we
proceed with $\dynv$ above

Finally we show $A \ltdyn \dynv$, $\u B \ltdyn \dync$ are admissible
by induction on $A$, $\u B$.

* If $A \in \{ \dynv, 0\}$ we use the primitive rule.

* If $A \not\in \{ \dynv, 0 \}$ we use the $A \ltdyn \dynv$ rule
and we need to show $A \ltdyn \floor A$. If $A = 1$, we use the
$1\ltdyn 1$ rule, otherwise we use the inductive hypothesis and

* If $\u B \in \{ \dync, \top\}$ we use the primitive rule.

* If $\u B \not\in \{ \dync, \top \}$ we use the $\u B \ltdyn
\dync$ rule and we need to show $\u B \ltdyn \floor {\u B}$, which
follows by inductive hypothesis and monotonicity.

Every other rule in Figure <ref> is a rule of
the normalized system in Figure <ref>.

Based on normalized type dynamism, we show

If $A \ltdyn A'$ according to Figure <ref>, then there is
a unique complex value $x : A \vdash \supcast{A}{A'}{x} : A'$
if $\u B \ltdyn \u B'$ according to Figure <ref>, then there is
a unique complex stack $x : \u B \vdash \supcast{\u B}{\u B'}{x} : \u B'$

§.§.§ Interpretation of Terms

Next, we extend the translation of casts to a translation of all terms
by congruence, since all terms in GTT besides casts are
in .  This satisfies:

If $\Gamma\pipe\Delta \vdash E : T$ in GTT, then $\sem{\Gamma}
\pipe\sem\Delta\vdash \sem E : \sem T$ in .

§.§.§ Interpretation of Term Dynamism

We have now given an interpretation of the types, terms, and
type dynamism proofs of GTT in .

To complete this to form a model of GTT, we need to give an
interpretation of the term dynamism proofs, which is
established by the
following “axiomatic graduality” theorem.

GTT has heterogeneous term dynamism
rules indexed by type dynamism, but   has only homogeneous
inequalities between terms, i.e., if $E \ltdyn E'$, then $E,E'$ have
the same context and types.

Since every type dynamism judgement has an associated contract, we can
translate a heterogeneous term dynamism to a homogeneous inequality
up to contract.  Our next overall goal is to prove

For any dynamic type interpretation,

\[
\inferrule
{\Phi : \Gamma \ltdyn \Gamma'\\
\Psi : \Delta \ltdyn \Delta'\\
\Phi \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'}
{\sem\Gamma \pipe \sem{\Delta'} \vdash \sem M[\sem{\Psi}] \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}]] : \sem{\u B}}
\quad
\inferrule
{\Phi : \Gamma \ltdyn \Gamma' \\
\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\sem{\Gamma} \vdash \supcast{A}{A'}[\sem{V}] \ltdyn\sem{V'}[\sem\Phi] : \sem {A'}}
\]

where we define $\sem{\Phi}$ to upcast each variable, and
$\sem{\Delta}$ to downcast $\bullet$ if it is nonempty, and if
$\Delta = \cdot$, then $M[\sem{\Delta}] = M$.

More explicitly,

* If $\Phi : \Gamma \ltdyn \Gamma'$, then there exists $n$
such that $\Gamma = x_1:A_1,\ldots,x_n:A_n$ and $\Gamma' =
x_1':A_1',\ldots,x_n':A_n'$ where $A_i \ltdyn A_i'$ for each
$i\leq n$.
Then $\sem{\Phi}$ is a substitution from $\sem{\Gamma}$ to $\sem{\Gamma'}$
defined as

\[ \sem{\Phi} = \supcast{A_1}{A_1'}x_1/x_1',\ldots\supcast{A_n}{A_n'}x_n/x_n' \]

* If $\Psi : \Delta \ltdyn \Delta'$, then we similarly define
$\sem{\Psi}$ as a “linear substitution”. That is, if $\Delta =
\Delta' = \cdot$, then $\sem{\Psi}$ is an empty substitution and
$M[\sem{\Psi}] = M$, otherwise $\sem{\Psi}$ is a linear
substitution from $\Delta' = \bullet : \u B'$ to $\Delta =
\bullet : \u B$ where $\u B \ltdyn \u B'$ defined as

\[ \sem\Psi = \sdncast{\u B}{\u B'}\bullet/\bullet \]

Relative to previous work on graduality <cit.>,
the distinction between complex value upcasts and complex stack
downcasts guides the formulation of the theorem; e.g. using upcasts in
the left-hand theorem would require more thunks/forces.

The full proof can be found in the extended version, and uses a
sequence of lemmas.  The first lemma shows that the translations of
casts in Figure <ref> do form ep pairs in the
sense of Definition <ref>.  One of the biggest
advantages of using an explicit syntax for complex values and complex
stacks is that the “shifted” casts (the downcast between $\u F$
types for $A \ltdyn A'$ and the upcast between $U$ types for $\u B
\ltdyn \u B'$) are the only effectful terms, and this lemma is the
only place where we need to reason about their definitions
explicitly—afterwards, we can simply use the fact that they are ep
pairs with the “pure” value upcasts and stack downcasts, which
compose much more nicely than effectful terms.  This is justified by two
additional lemmas, which show that a projection is determined
by its embedding and vice versa, and that embedding-projections
satisfy an adjunction/Galois connection property.  The final lemmas
show that, according to Figure <ref>,
$\supcast{A}{A'}$ is equivalent to the identity and
$\supcast{A'}{A''}\supcast{A}{A'}$ is $\supcast{A}{A''}$, and
similarly for downcasts.  All of these properties are theorems in GTT
(Section <ref>), and in the extended version it
takes quite a bit of work to prove them true under translation, which
illustrates that the axiomatic theory of GTT encodes a lot of
information with relatively few rules.

We now develop some lemmas on the way towards proving this result.
First, to keep proofs high-level, we establish the following cast
reductions that follow easily from $\beta,\eta$ principles.

The following are all provable

\begin{align*}
&\sem{\upcast{A_1+A_2}{A_1'+A_2'}}[\inl V] \equidyn \inl \sem{\upcast{A_1}{A_1'}}[V]\\
&\sem{\upcast{A_1+A_2}{A_1'+A_2'}}[\inr V] \equidyn \inr \sem{\upcast{A_2}{A_2'}}[V]\\
&\sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \inl V] \equidyn
\bindXtoYinZ {\sem{\dncast{A_1}{A_1'}}[\ret V]} {x_1} \ret \inl x_1\\
&\sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \inr V] \equidyn
\bindXtoYinZ {\sem{\dncast{A_2}{A_2'}}[\ret V]} {x_2} \ret \inr x_2\\
&\sem{\dncast{\u F 1}{\u F1}} \equidyn \bullet\\
&\sem{\upcast{ 1}{1}}[x] \equidyn x\\
&\sem{\dncast{\u F(A_1\times A_2)}{\u F(A_1'\times A_2')}}[\ret (V_1,V_2)]\\
\bindXtoYinZ {\sdncast{\u FA_1}{\u F A_1'}[\ret V_1]} {x_1} \bindXtoYinZ {\sdncast{\u FA_2}{\u F A_2'}[\ret V_2]} {x_2} \ret (x_1,x_2)\\
&\supcast{A_1\times A_2}{A_1'\times A_2'}[(V_1,V_2)] \equidyn (\supcast{A_1}{A_1'}[V_1], \supcast{A_2}{A_2'}[V_2])\\
&(\sdncast{A \to \u B}{A' \to \u B'} M)\, V \equidyn
(\sdncast{\u B}{\u B'} M)\, (\supcast{A}{A'}{V})\\
&(\force (\supcast{U(A\to\u B)}{U(A'\to\u B')} V))\,V'\\
\bindXtoYinZ {\dncast{\u FA}{\u FA'}[\ret V']} x {\force (\supcast{U\u B}{U\u B'}{(\thunk (\force V\, x))})}\\
&\pi \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} M \equidyn
\sdncast{\u B_1}{\u B_1'} \pi M\\
&\pi' \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} M \equidyn
\sdncast{\u B_2}{\u B_2'} \pi' M\\
&\pi \force (\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')} V)
\equidyn
\force \supcast{U\u B_1}{U\u B_1'}{\thunk (\pi \force V)}\\
&\pi' \force (\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')} V)
\equidyn
\force \supcast{U\u B_2}{U\u B_2'}{\thunk (\pi' \force V)}\\
&\sdncast{\u F U \u B}{\u F U \u B'}[\ret V] \equidyn \ret\thunk \sdncast{\u B}{\u B'}\force V\\
&\force \supcast{U\u FA}{U \u F A'}[V]
\equidyn
\bindXtoYinZ {\force V} x \thunk\ret\upcast{A}{A'} x
\end{align*}

Our next goal is to show that from the basic casts being ep pairs, we
can prove that all casts as defined in Figure <ref>
are ep pairs.  Before doing so, we prove the following lemma, which is
used for transitivity (e.g. in the $A \ltdyn \dynv$ rule, which uses a
composition $A \ltdyn \floor{A} \ltdyn \dynv$):

* If $(V_1, S_1)$ is a value ep pair from $A_1$ to $A_2$ and
$(V_2,S_2)$ is a value ep pair from $A_2$ to $A_3$, then
$(V_2[V_1], S_1[S_2])$ is a value ep pair from $A_1$ to $A_3$.

* If $(V_1, S_1)$ is a computation ep pair from $\u B_1$ to $\u B_2$ and
$(V_2,S_2)$ is a computation ep pair from $\u B_2$ to $\u B_3$, then
$(V_2[V_1], S_1[S_2])$ is a computation ep pair from $\u B_1$ to $\u B_3$.

* First, retraction follows from retraction twice:

\[ S_1[S_2[\ret V_2[V_1[x]]]] \equidyn S_1[\ret [V_1[x]]] \equidyn x \]

and projection follows from projection twice:

\begin{align*}
\bindXtoYinZ {S_1[S_2[\bullet]]} x \ret V_2[V_1[x]]
{\bindXtoYinZ {S_1[S_2[\bullet]]} x \bindXtoYinZ {\ret [V_1[x]]} y \ret V_2[y]}\tag{$\u F\beta$}\\
\bindXtoYinZ {(\bindXtoYinZ {S_1[S_2[\bullet]]} x {\ret [V_1[x]]})} y \ret V_2[y]\tag{Commuting conversion}\\
\bindXtoYinZ {S_2[\bullet]} y \ret V_2[y]\tag{Projection}\\
&\ltdyn \bullet \tag{Projection}
\end{align*}

* Again retraction follows from retraction twice:

\[ S_1[S_2[\force V_2[V_1[z]]]] \equidyn S_1[\force V_1[z]] \equidyn \force z \]

and projection from projection twice:

\begin{align*}
V_2[V_1[\thunk S_1[S_2[\force w]]]]
&\equidyn V_2[V_1[\thunk S_1[\force \thunk S_2[\force w]]]]\tag{$U\beta$}\\
&\ltdyn V_2[\thunk S_2[\force w]] \tag{Projection}\\
&\ltdyn w \tag{Projection}
\end{align*}

$(x. x, \bullet)$ is an ep pair (value or computation).

Now, we show that all casts are ep pairs.

The proof is a somewhat tedious, but straightforward calculation.

* For any $A \ltdyn A'$, the casts $(x.\sem{\upcast{A}{A'}x},
\sem{\dncast{\u F A}{\u F A'}})$ are a value ep pair from
$\sem{A}$ to $\sem{A'}$

* For any $\u B \ltdyn \u B'$, the casts $(z. \sem{\upcast{U \u
B}{U \u B'}z}, \sem{\dncast{\u B}{\u B'}})$ are a computation ep
pair from $\sem{\u B}$ to $\sem{\u B'}$.

By induction on normalized type dynamism derivations.

* $A \ltdyn A$ ($A \in \{\dyn, 1\}$), because identity is an ep pair.

* $0 \ltdyn A$ (that $A \in \{ \dyn, 0 \}$ is not important):

* Retraction is

\[ x : 0 \vdash \ret x \equidyn \bindXtoYinZ {\ret\absurd x} y \err : \u F A \]

which holds by $0\eta$

* Projection is

\[ \bullet : \u F A \vdash \bindXtoYinZ {(\bindXtoYinZ \bullet y \err)} x {\ret\absurd x} \ltdyn \bullet : \u F A \]

Which we calculate:

\begin{align*}
&\bindXtoYinZ {(\bindXtoYinZ \bullet y \err)} x {\ret\absurd x}\\
&\equidyn \bindXtoYinZ \bullet y \bindXtoYinZ \err x {\ret\absurd x}\tag{comm conv}\\
&\equidyn \bindXtoYinZ \bullet y \err \tag{Strictness of Stacks}\\
&\ltdyn \bindXtoYinZ \bullet y \ret y \tag{$\err$ is $\bot$}\\
&\equidyn \bullet \tag{$\u F\eta$}
\end{align*}

* $+$:

* Retraction is

\begin{align*}
&x : A_1 + A_2 \vdash\\
&\sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \sem{\upcast{A_1+A_2}{A_1'+A_2'}}[x]]\\
&=\sdncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}[\ret\caseofXthenYelseZ x {x_1. \inl\supcast{A_1}{A_1'}[x_1]}{x_1. \inr\supcast{A_2}{A_2'}[x_2]}]\\
\caseofX x\tag{commuting conversion}\\
&\quad\thenY {x_1. \sdncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}[\ret\inl\supcast{A_1}{A_1'}[x_1]]}\\
&\quad\elseZ {x_2. \sdncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}[\ret\inr\supcast{A_2}{A_2'}[x_2]]}\\
\caseofX x\tag{cast computation}\\
&\quad\thenY{x_1. \bindXtoYinZ {\sdncast{\u F A_1}{\u F A_1'}[\ret \supcast{A_1}{A_1'}x_1]} {x_1} \ret \inl x_1}\\
&\quad\elseZ{x_2. \bindXtoYinZ {\sdncast{\u F A_2}{\u F A_2'}[\ret \supcast{A_2}{A_2'}x_2]} {x_2} \ret \inr x_2}\\
&\equidyn \caseofXthenYelseZ x {x_1. \ret \inl x_1} {x_2. \ret \inr x_2}\tag{IH retraction}\\
&\equidyn \ret x\tag{$+\eta$}
\end{align*}

* For Projection:

\begin{align*}
&\bullet : A_1' + A_2' \vdash\\
&\bindXtoYinZ {\sdncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}} x \supcast{A_1+A_2}{A_1'+A_2'}[x]\\
\bindXtoYinZ {(\bindXtoYinZ \bullet {x'} \caseofXthenYelseZ {x'} {x_1'. \bindXtoYinZ {\sem{\dncast{\u FA_1}{\u FA_1'}}[\ret x_1']} {x_1} \ret\inl x_1}{x_2'. \cdots})} x\\
\bindXtoYinZ \bullet x' \caseofX {x'} \tag{Commuting Conversion}\\
&\qquad \thenY {x_1'. \bindXtoYinZ {\sem{\dncast{\u FA_1}{\u FA_1'}}[\ret x_1']} {x_1} \supcast{A_1+A_2}{A_1'+A_2'}{\ret\inl x_1}}\\
&\qquad \elseZ {x_2'. \bindXtoYinZ {\sem{\dncast{\u FA_2}{\u FA_2'}}[\ret x_2']} {x_2} \supcast{A_1+A_2}{A_1'+A_2'}{\ret\inr x_2}}\\
\bindXtoYinZ \bullet x' \caseofX {x'}\tag{Cast Computation}\\
&\qquad \thenY {x_1'. \bindXtoYinZ {\sem{\dncast{\u FA_1}{\u FA_1'}}[\ret x_1']} {x_1} {\ret\inl \supcast{A_1}{A_1'}x_1}}\\
&\qquad \elseZ {x_2'. \bindXtoYinZ {\sem{\dncast{\u FA_2}{\u FA_2'}}[\ret x_2']} {x_2} {\ret\inr \supcast{A_2}{A_2'}x_2}}\\
\bindXtoYinZ \bullet x' \caseofXthenYelseZ {x'} {x_1'. \ret\inl x_1'} {x_2'. \ret \inr x_2'}\tag{IH projection}\\
&\equidyn \bindXtoYinZ \bullet x' \ret x'\tag{$+\eta$}\\
&\equidyn \bullet \tag{$\u F\eta$}\\
\end{align*}

* $\times$:

* First, Retraction:

\begin{align*}
&x : A_1\times A_2 \vdash\\
&\sdncast{\u F(A_1\times A_2)}{\u F(A_1'\times A_2')}[\ret \supcast{A_1\times A_2}{A_1' \times A_2'}[x]]\\
&=\sdncast{\u F(A_1\times A_2)}{\u F(A_1'\times A_2')}[\ret\pmpairWtoXYinZ x {x_1}{x_2} (\supcast{A_1}{A_1'}[x_1], \supcast{A_2}{A_2'}[x_2])]\\
\pmpairWtoXYinZ x {x_1} {x_2} \sdncast{\u F(A_1\times A_2)}{\u F(A_1'\times A_2')}[\ret(\supcast{A_1}{A_1'}[x_1], \supcast{A_2}{A_2'}[x_2])]\tag{commuting conversion}\\
\pmpairWtoXYinZ x {x_1} {x_2} \tag{cast reduction}\\
&\quad\bindXtoYinZ {\sdncast{\u F A_1}{\u F A_1'}[\ret\supcast{A_1}{A_1'}[x_1]]} {y_1}\\
&\quad\bindXtoYinZ {\sdncast{\u F A_2}{\u F A_2'}[\ret\supcast{A_2}{A_2'}[x_2]]} {y_2}\\
&\quad\ret(y_1, y_2)\\
\pmpairWtoXYinZ x {x_1} {x_2} \bindXtoYinZ {\ret x_1} {y_1} \bindXtoYinZ {\ret x_2} {y_2} \ret(y_1, y_2)\tag{IH retraction}\\
\pmpairWtoXYinZ x {x_1} {x_2} \ret(x_1,x_2) \tag{$\u F\beta$}\\
&\equidyn \ret x\tag{$\times\eta$}
\end{align*}

* Next, Projection:

\begin{align*}
&\bullet : \u F A'\vdash\\
&\bindXtoYinZ {\sdncast{\u F(A_1\times A_2)}{\u F(A_1'\times A_2')}[\bullet]} x \ret\supcast{A_1\times A_2}{A_1' \times A_2'}[x]\\
&\equidyn\bindXtoYinZ \bullet {x'} \pmpairWtoXYinZ {{x'}} {x_1'}{x_2'} \tag{$\u F\eta, \times\eta$}\\
&\quad \bindXtoYinZ {\sdncast{\u F(A_1\times A_2)}{\u F(A_1'\times A_2')}[\ret (x_1',x_2')]} x\\
&\quad \ret\supcast{A_1\times A_2}{A_1' \times A_2'}[x]\\
&\equidyn\bindXtoYinZ \bullet {x'} \pmpairWtoXYinZ {{x'}} {x_1'}{x_2'}\tag{cast reduction}\\
&\quad \bindXtoYinZ {\sdncast{\u F A_1}{\u F A_1'}[\ret x_1']} {x_1}\\
&\quad \bindXtoYinZ {\sdncast{\u F A_2}{\u F A_2'}[\ret x_2']} {x_2}\\
&\quad \ret\supcast{A_1\times A_2}{A_1' \times A_2'}[(x_1,x_2)]\\
&\equidyn\bindXtoYinZ \bullet {x'} \pmpairWtoXYinZ {{x'}} {x_1'}{x_2'}\tag{cast reduction}\\
&\quad \bindXtoYinZ {\sdncast{\u F A_1}{\u F A_1'}[\ret x_1']} {x_1}\\
&\quad \bindXtoYinZ {\sdncast{\u F A_2}{\u F A_2'}[\ret x_2']} {x_2}\\
&\quad \ret(\supcast{A_1}{A_1'}[x_1], \supcast{A_2}{A_2'}[x_2])\\
&\equidyn\bindXtoYinZ \bullet {x'} \pmpairWtoXYinZ {{x'}} {x_1'}{x_2'}\tag{$\u F \beta$, twice}\\
&\quad \bindXtoYinZ {\sdncast{\u F A_1}{\u F A_1'}[\ret x_1']} {x_1}\\
&\quad \bindXtoYinZ {\sdncast{\u F A_2}{\u F A_2'}[\ret x_2']} {x_2}\\
&\quad \bindXtoYinZ {\ret \supcast{A_2}{A_2'}[x_2]}{y_2'}\\
&\quad \bindXtoYinZ {\ret \supcast{A_1}{A_1'}[x_1]}{y_1'}\\
&\quad \ret(y_1',y_2')\\
&\ltdyn\bindXtoYinZ \bullet {x'} \pmpairWtoXYinZ {{x'}} {x_1'}{x_2'}\tag{IH Projection}\\
&\quad \bindXtoYinZ {\sdncast{\u F A_1}{\u F A_1'}[\ret x_1']} {x_1}\\
&\quad \bindXtoYinZ {\ret x_2'} {y_2'}\\
&\quad \bindXtoYinZ {\ret \supcast{A_1}{A_1'}[x_1]} {y_1'}\\
&\quad \ret(y_1',y_2')\\
&\equidyn\bindXtoYinZ \bullet {x'} \pmpairWtoXYinZ {{x'}} {x_1'}{x_2'}\tag{$\u F\beta$}\\
&\quad \bindXtoYinZ {\sdncast{\u F A_1}{\u F A_1'}[\ret x_1']} {x_1}\\
&\quad \bindXtoYinZ {\ret \supcast{A_1}{A_1'}[x_1]} {y_1'}\\
&\quad \ret(x_1',y_2')\\
&\ltdyn\bindXtoYinZ \bullet {x'} \pmpairWtoXYinZ {{x'}} {x_1'}{x_2'}\tag{IH Projection}\\
&\quad \bindXtoYinZ {\ret x_1'} {y_1'}\\
&\quad \ret(x_1',y_2')\\
&\equidyn\bindXtoYinZ \bullet {x'} \pmpairWtoXYinZ {{x'}} {x_1'}{x_2'}
\ret(x_1',x_2')\tag{$\u F\beta$}\\
&\equidyn\bindXtoYinZ \bullet {x'} \ret {x'}\tag{$\times\eta$}\\
&\equidyn\bullet \tag{$\u F \eta$}
\end{align*}

* $U$: By inductive hypothesis, $(x.\sem{\upcast{U\u B}{U\u
B'}}, \dncast{\u B}{\u B'})$ is a computation ep pair

* To show retraction we need to prove:

\[
x : U \u B \vdash \ret x \equidyn \bindXtoYinZ {(\ret \thunk {\sem{\upcast{U\u B}{U \u B'}}})} y {\ret \thunk \sem{\dncast{\u B}{\u B'}}[\force y]} : \u F U \u B'
\]

Which we calculate as follows:

\begin{align*}
&x : U\u B \vdash \\
&\sdncast{\u FU\u B}{\u FU\u B'}[{(\ret {\sem{\upcast{U\u B}{U \u B'}}[x]})}]\\
\ret\thunk(\sdncast{\u B}{\u B'}[\force {\sem{\upcast{U\u B}{U \u B'}}}[x]])\tag{Cast Reduction}\\
&\equidyn \ret\thunk \force x \tag{IH Retraction}\\
&\equidyn \ret x \tag{$U\eta$}
\end{align*}

* To show projection we calculate:

\begin{align*}
&\bindXtoYinZ {\sdncast{\u FU\u B}{\u FU\u B'}[\bullet]} x \supcast{U\u B}{U\u B'}[x]\\
\bindXtoYinZ \bullet {x'} \bindXtoYinZ {\sdncast{\u FU\u B}{\u FU\u B'}[\ret x']} x \supcast{U\u B}{U\u B'}[x]\tag{$\u F\eta$}\\
\bindXtoYinZ \bullet {x'} \bindXtoYinZ {\ret\thunk(\sdncast{\u B}{\u B'}[\force x'])} x \supcast{U\u B}{U\u B'}[x]\tag{Cast Reduction}\\
\bindXtoYinZ \bullet {x'} \supcast{U\u B}{U\u B'}[\thunk(\sdncast{\u B}{\u B'}[\force x'])] \tag{$\u F\beta$}\\
&\ltdyn \bindXtoYinZ \bullet {x'} x'\tag{IH Projection}\\
&\equidyn \bullet \tag{$\u F\eta$}
\end{align*}

* There's a few base cases about the dynamic computation type, then

* $\top$:

* Retraction is by $\top\eta$:

\begin{align*}
z : U \top \vdash \force z \equidyn \{ \} : \top
\end{align*}

* Projection is

\begin{align*}
\thunk \err
&\ltdyn \thunk \force w \tag{$\err$ is $\bot$}\\
&\equidyn w \tag{$U\eta$}
\end{align*}

* $\with$:

* Retraction

\begin{align*}
&z : U (\u B_1 \with \u B_2)\vdash \\
&\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\force \supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')}[z]]\\
\pairone{\pi\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\force \supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')}[z]]} \tag{$\with\eta$}\\
&\qquad\pairtwo{\pi' \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\force \supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')}[z]]}\\
\pairone{\sdncast{\u B_1}{\u B_1'}[\pi\force \supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')}[z]]} \tag{Cast reduction}\\
&\qquad\pairtwo{\sdncast{\u B_2}{\u B_2'}[\pi'\force \supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')}[z]]}\\
\pairone{\sdncast{\u B_1}{\u B_1'}[\force\supcast{U\u B_1}{U\u B_1'}[\thunk \pi \force z]]} \tag{Cast reduction}\\
& \qquad\pairtwo{\sdncast{\u B_2}{\u B_2'}[\force\supcast{U\u B_2}{U\u B_2'}[\thunk \pi' \force z]]}\\
\pair{\force \thunk \pi \force z}{\force \thunk \pi' \force z} \tag{IH retraction}\\
&\equidyn \pair{\pi \force z}{\pi' \force z}\tag{$U\beta$}\\
&\equidyn \force z \tag{$\with\eta$}
\end{align*}

* Projection

\begin{align*}
&w : U {\u B_1' \with \u B_2'} \vdash\\
& \supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')}[\thunk \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\force w]]\\
\thunk\force\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')}[\thunk \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\force w]]\tag{$U\eta$}\\
\thunk\pairone{\pi\force\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')}[\thunk \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\force w]]}\\
&\qquad\qquad\pairtwo{\pi'\force\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')}[\thunk \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\force w]]}\tag{$\with\eta$}\\
\thunk\pairone{\force\supcast{U\u B_1}{U\u B_1'}[\thunk\pi\force\thunk \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\force w]]}\\
&\qquad\qquad\pairtwo{\force\supcast{U\u B_2}{U\u B_2'}[\thunk\pi'\force\thunk \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\force w]]}\tag{cast reduction}\\
\thunk\pairone{\force\supcast{U\u B_1}{U\u B_1'}[\thunk\pi \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\force w]]} \tag{$U\beta$}\\
&\qquad\qquad\pairtwo{\force\supcast{U\u B_2}{U\u B_2'}[\thunk\pi' \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\force w]]}\\
\thunk\pairone{\force\supcast{U\u B_1}{U\u B_1'}[\thunk\sdncast{\u B_1}{\u B_1'}[\pi\force w]]} \tag{cast reduction}\\
&\qquad\qquad\pairtwo{\force\supcast{U\u B_2}{U\u B_2'}[\thunk\sdncast{\u B_2}{\u B_2'}[\pi'\force w]]}\\
\thunk\pairone{\force\supcast{U\u B_1}{U\u B_1'}[\thunk\sdncast{\u B_1}{\u B_1'}[\force\thunk\pi\force w]]} \tag{$U\beta$}\\
&\qquad\qquad\pairtwo{\force\supcast{U\u B_2}{U\u B_2'}[\thunk\sdncast{\u B_2}{\u B_2'}[\force\thunk\pi'\force w]]}\\
\thunk\pair{\force\thunk\pi\force w}{\force\thunk\pi'\force w} \tag{IH projection}\\
\thunk\pair{\pi\force w}{\pi'\force w} \tag{$U\beta$}\\
&\equidyn \thunk\force w \tag{$\with\eta$}\\
&\equidyn w \tag{$U\eta$}\\
\end{align*}

* $\to$:

* Retraction

\begin{align*}
&z : U (A \to \u B)\vdash \\
&\sdncast{A \to \u B}{A' \to \u B'}[\force \supcast{U(A \to \u B)}{U(A' \to \u B')}[z]]\\
\lambda x:A. (\sdncast{A \to \u B}{A' \to \u B'}[\force \supcast{U(A \to \u B)}{U(A' \to \u B')}[z]])\,x\tag{$\to\eta$}\\
\lambda x:A.
\sdncast{\u B}{\u B'}[(\force \supcast{U(A \to \u B)}{U(A' \to \u B')}[z])(\supcast{A}{A'}[x])] \tag{cast reduction}\\
\lambda x:A.\tag{cast reduction}\\
\sdncast{\u B}{\u B'}[\bindXtoYinZ{\sdncast{\u F A}{\u F A'}[\ret \upcast{A}{A'}[x]]} {y} \force \upcast{U \u B}{U\u B'}[\thunk((\force z)\, y)]]\\
\lambda x:A. \sdncast{\u B}{\u B'}[\bindXtoYinZ{\ret x} {y} \force \upcast{U \u B}{U\u B'}[\thunk((\force z)\, y)]]\tag{IH Retraction}\\
\lambda x:A. \sdncast{\u B}{\u B'}[\force \upcast{U \u B}{U\u B'}[\thunk((\force z)\, x)]]\tag{$\u F\beta$}\\
&\equidyn \lambda x:A. \force \thunk((\force z)\, x) \tag{IH retraction}\\
&\equidyn \lambda x:A. (\force z)\, x \tag{$U\beta$}\\
&\equidyn \force z \tag{$\to\eta$}\\
\end{align*}

* Projection

\begin{align*}
&w : U (A' \to \u B') \vdash\\
& \supcast{U(A \to \u B)}{U(A' \to \u B')}[\thunk \sdncast{A \to \u B}{A' \to \u B'}[\force w]]\\
\thunk\force\supcast{U(A \to \u B)}{U(A' \to \u B')}[\thunk \sdncast{A \to \u B}{A' \to \u B'}[\force w]]\tag{$U\eta$}\\
\thunk\lambda x':A'.\\
&\quad(\force\supcast{U(A \to \u B)}{U(A' \to \u B')}[\thunk \sdncast{A \to \u B}{A' \to \u B'}[\force w]])\,x'\tag{$\to\eta$}\\
&\equidyn \thunk\lambda x':A'.\\
&\qquad \bindXtoYinZ {\sdncast{\u F A}{\u F A'}[\ret x']} x\tag{cast reduction}\\
\force\supcast{U\u B}{U \u B'}[\thunk((\force \thunk \sdncast{A \to \u B}{A' \to \u B'}[\force w])\, x)]\\
&\equidyn \thunk\lambda x':A'.\\
&\qquad \bindXtoYinZ {\sdncast{\u F A}{\u F A'}[\ret x']} x\tag{$U\beta$}\\
\force\supcast{U\u B}{U \u B'}[\thunk((\sdncast{A \to \u B}{A' \to \u B'}[\force w])\, x)]\\
\thunk\lambda x':A'.\\
&\qquad \bindXtoYinZ {\sdncast{\u F A}{\u F A'}[\ret x']} x\tag{cast reduction}\\
\force\supcast{U\u B}{U \u B'}[\thunk\sdncast{\u B}{\u B'}[(\force w)\,(\upcast{A}{A'}[x])]]\\
\thunk\lambda x':A'.\\
&\qquad\bindXtoYinZ {\sdncast{\u F A}{\u F A'}[\ret x']} x\tag{$\u F\beta$}\\
&\qquad\bindXtoYinZ {\ret{\upcast{A}{A'}[x]}} {x'}\\
&\qquad\force\supcast{U\u B}{U \u B'}[\thunk\sdncast{\u B}{\u B'}[(\force w)\,x']]\\
\thunk\lambda x':A'.\tag{IH projection}\\
&\qquad\bindXtoYinZ {\ret x'} {x'}\\
&\qquad\force\supcast{U\u B}{U \u B'}[\thunk\sdncast{\u B}{\u B'}[(\force w)\,x']]\\
\thunk\lambda x':A'.
\force\supcast{U\u B}{U \u B'}[\thunk\sdncast{\u B}{\u B'}[(\force w)\,x']]\tag{$\u F\beta$}\\
\thunk\lambda x':A'.
\force\supcast{U\u B}{U \u B'}[\thunk\sdncast{\u B}{\u B'}[\force\thunk((\force w)\,x')]]\tag{$\u F\beta$}\\
\thunk\lambda x':A'. \force\thunk((\force w)\,x')\tag{IH projection}\\
&\equidyn \thunk\lambda x':A'. ((\force w)\,x')\tag{$U\beta$}\\
&\equidyn \thunk\force w\tag{$\to\eta$}\\
&\equidyn w \tag{$U\eta$}\\
\end{align*}

* $\u F$:

* To show retraction we need to show

\[
z : U \u F A \vdash
\force z \equidyn
\sem{\dncast{\u F A}{\u F A'}}[\force \thunk (\bindXtoYinZ {\force z} x \ret \sem{\upcast{A}{A'}})]
\]

We calculate:

\begin{align*}
&\sem{\dncast{\u F A}{\u F A'}}[\force \thunk (\bindXtoYinZ {\force z} x \ret \sem{\upcast{A}{A'}})]\\
\sem{\dncast{\u F A}{\u F A'}}[(\bindXtoYinZ {\force z} x \ret \sem{\upcast{A}{A'}})]\tag{$U\beta$}\\
\bindXtoYinZ {\force z} x \sem{\dncast{\u F A}{\u F A'}}[\ret \sem{\upcast{A}{A'}}] \tag{comm conv}\\
\bindXtoYinZ {\force z} x \ret x \tag{IH value retraction}\\
&\equidyn \force z \tag{$\u F\eta$}
\end{align*}

* To show projection we need to show

\[
w : U \u F A' \vdash
\thunk {(\bindXtoYinZ {\force {\thunk \sem{\dncast{\u F A}{\u F A'}}[\force w]}} x \ret \sem{\upcast{A}{A'}})}
\ltdyn w : U \u B'
\]

We calculate as follows

\begin{align*}
&\thunk {(\bindXtoYinZ {\force {\thunk \sem{\dncast{\u F A}{\u F A'}}[\force w]}} x \ret \sem{\upcast{A}{A'}})}\\
&\equidyn\thunk {(\bindXtoYinZ {{\sem{\dncast{\u F A}{\u F A'}}[\force w]}} x \ret \sem{\upcast{A}{A'}})} \tag{$U\beta$}\\
&\ltdyn \thunk {\force w} \tag{IH value projection}\\
& \equidyn w \tag{$U\eta$}
\end{align*}

While the above was tedious, this pays off greatly in later proofs: this
is the only proof in the entire development that needs to inspect
the definition of a “shifted” cast (a downcast between $\u F$ types or
an upcast between $U$ types).

All later lemmas

have cases for these shifted casts, but only use the property
that they are part of an ep pair.

This is one of the biggest advantages of using an explicit syntax for
complex values and complex stacks: the shifted casts are the only ones
that non-trivially use effectful terms, so after this lemma is
established we only have to manipulate values and stacks, which
compose much more nicely than effectful terms.

Conceptually, the main reason we can avoid reasoning about the
definitions of the shifted casts directly is that any two shifted casts
that form an ep pair with the same value embedding/stack projection are

For any value $x : A \vdash V_e : A'$ and stacks $\bullet : \u F A'
\vdash S_1 : \u F A$ and $\bullet : \u F A' \vdash S_2 : \u F A$, if
$(V_e, S_1)$ and $(V_e, S_2)$ are both value ep pairs, then

\[ S_1 \equidyn S_2 \]

Similarly for any values $x : U\u B \vdash V_1 : U \u B'$ and $x :
U\u B \vdash V_2 : U \u B'$ and stack $\bullet : \u B' \vdash S_p :
\u B$, if $(V_1, S_p)$ and $(V_2, S_p)$ are both computation ep pairs then

\[ V_1 \equidyn V_2 \]

By symmetry it is sufficient to show $S_1 \ltdyn S_2$.

S_1 S_1
S_1 x x ∙x S_1[x]
S_1 x V_e ∙x x
S_1 x x ∙x S_2[x]
∙: F̆ A' ⊢S_1 S_2 : F̆ A

similarly to show $V_1 \ltdyn V_2$:

x : U B̆ ⊢V_2 V_2 : U B̆'
x : U B̆ ⊢x S_p[V_2]
x : U B̆ ⊢V_1 V_2 : U B̆'
x : U B̆ ⊢V_1 V_2 : U B̆'

The next two lemmas on the way to axiomatic graduality show that
Figure <ref> translates $\upcast{A}{A}$ to the
identity and $\upcast{A'}{A''}{\upcast{A}{A'}}$ to the same contract as
$\upcast{A}{A''}$, and similarly for downcasts.

Intuitively, for all connectives except $\u F, U$, this is because of
functoriality of the type constructors on values and stacks.

For the $\u F, U$ cases, we will use the corresponding fact about the
dual cast, i.e., to prove the $\u F A$ to $\u F A$ downcast is the
identity stack, we know by inductive hypothesis that the $A$ to $A$
upcast is the identity, and that the identity stack is a projection
for the identity.

Therefore Lemma <ref> implies that the $\u
FA$ downcast must be equivalent to the identity.
We now discuss these two lemmas and their proofs in detail.

First, we show that the casts from a type to itself are equivalent to
the identity.

Below, we will use this lemma to prove the reflexivity case of the
axiomatic graduality theorem, and to prove a conservativity result,
which says that a GTT homogeneous term dynamism is the same as a
inequality between their translations.

For any $A$ and $\u B$,

x:A ⊢AA x : A∙: B̆ ⊢B̆B̆ ∙: B̆

We proceed by induction on $A, \u B$, following the proof that
reflexivity is admissible given in Lemma <ref>.

* If $A \in \{1, \dynv \}$, then $\supcast{A}{A}[x] = x$.

* If $A = 0$, then $\absurd x \equidyn x$ by $0\eta$.

* If $A = U \u B$, then by inductive hypothesis $\sdncast{\u
B}{\u B} \equidyn \bullet$. By Lemma <ref>,
$(x. x, \bullet)$ is a computation ep pair from $\u B$ to
itself. But by Lemma <ref>, $(\supcast{U\u
B}{U\u B}[x], \bullet)$ is also a computation ep pair so the
result follows by uniqueness of embeddings from computation
projections Lemma <ref>.

* If $A = A_1\times A_2$ or $A = A_1+A_2$, the result follows by
the $\eta$ principle and inductive hypothesis.

* If $\u B = \dync$, $\sdncast{\dync}{\dync} = \bullet$.

* For $\u B = \top$, the result follows by $\top\eta$.

* For $\u B = \u B_1 \with \u B_2$ or $\u B = A \to \u B'$, the
result follows by inductive hypothesis and $\eta$.

* For $\u B = \u FA$, by inductive hypothesis, the downcast is a
projection for the value embedding $x.x$, so the result follows by
identity ep pair and uniqueness of projections from value

Second, we show that a composition of upcasts is translated to the same
thing as a direct upcast, and similarly for downcasts.  Below, we will
use this lemma to translate transitivity of term dynamism in GTT.

For any dynamic type interpretation $\rho$,

A A' A”
x : A ⊢A A” A' A”[A A'] : A”

B̆ B̆' B̆”
∙: B̆” ⊢B̆B̆” B̆B̆'[B̆'B̆”]

By mutual induction on $A, \u B$.

* $A \ltdyn A' \ltdyn A''$

* If $A = 0$, we need to show $x : 0 \vdash
\supcast{0}{A''}[x] \equidyn
\supcast{A'}{A''}[\supcast{0}{A'}[x]] : A''$ which follows by

* If $A = \dynv$, then $A' = A'' = \dynv$, and both casts are
the identity.

* If $A \not\in \{\dynv, 0 \}$ and $A' = \dynv$, then $A'' =
\dynv$ and $\supcast{\dynv}{\dynv}[\supcast{A}{\dynv}] =
\supcast{A}{\dynv}$ by definition.

* If $A, A' \not\in \{\dynv, 0 \}$ and $A'' = \dynv$, then
$\floor A = \floor {A'}$, which we call $G$ and

\[ \supcast{A}{\dynv} = \supcast{G}{\dynv}[\supcast{A}{G}] \]

\[ \supcast{A'}{\dynv}[\supcast{A}{A'}] = \supcast{G}{\dynv}[\supcast{A'}{G}[\supcast{A}{A'}]] \]

so this reduces to the case for $A \ltdyn A' \ltdyn G$, below.

* If $A,A',A'' \not\in \{\dynv, 0 \}$, then they all have the same
top-level constructor:

* $+$: We need to show for $A_1 \ltdyn A_1' \ltdyn A_1''$
and $A_2 \ltdyn A_2' \ltdyn A_2''$:

\[
x : \sem{A_1} + \sem{A_2} \vdash
\supcast{A_1'+A_2'}{A_1''+A_2''}[\supcast{A_1+A_2}{A_1'+A_2'}[x]]\equidyn
\supcast{A_1+A_2}{A_1''+A_2''}[x]
: \sem{A_1''}+\sem{A_2''}.
\]

We proceed as follows:

\begin{align*}
&\equidyn \caseofX {x}\tag{$+\eta$}\\
&\qquad\thenY {x_1. \supcast{A_1'+A_2'}{A_1''+A_2''}[\supcast{A_1+A_2}{A_1'+A_2'}[\inl x_1]]}\\
&\qquad\elseZ {x_2. \supcast{A_1'+A_2'}{A_1''+A_2''}[\supcast{A_1+A_2}{A_1'+A_2'}[\inr x_2]]}\\
&\equidyn \caseofX {x}\tag{cast reduction}\\
&\qquad\thenY {x_1. \supcast{A_1'+A_2'}{A_1''+A_2''}[\inl\supcast{A_1}{A_1'}[x_1]]}\\
&\qquad\elseZ {x_2. \supcast{A_1'+A_2'}{A_1''+A_2''}[\inr\supcast{A_2}{A_2'}[x_2]]}\\
&\equidyn \caseofX {x}\tag{cast reduction}\\
&\qquad\thenY {x_1. \inl\supcast{A_1'}{A_1''}[\supcast{A_1}{A_1'}[x_1]]}\\
&\qquad\elseZ {x_2. \inr\supcast{A_2'}{A_2''}[\supcast{A_2}{A_2'}[x_2]]}\\
&\equidyn \caseofX {x}\tag{IH}\\
&\qquad\thenY {x_1. \inl\supcast{A_1}{A_1''}[x_1]}\\
&\qquad\elseZ {x_2. \inr\supcast{A_2}{A_2''}[x_2]}\\
&= \supcast{A_1+A_2}{A_1''+A_2''}[x] \tag{definition}
\end{align*}

* $1$: By definition both sides are the identity.

* $\times$: We need to show for $A_1 \ltdyn A_1' \ltdyn A_1''$
and $A_2 \ltdyn A_2' \ltdyn A_2''$:

\[
x : \sem{A_1} \times \sem{A_2} \vdash
\supcast{A_1'\times A_2'}{A_1''\times A_2''}[\supcast{A_1\times A_2}{A_1'\times A_2'}[x]]\equidyn
\supcast{A_1\times A_2}{A_1''\times A_2''}[x]
: \sem{A_1''}\times \sem{A_2''}.
\]

We proceed as follows:

\begin{align*}
&\supcast{A_1'\times A_2'}{A_1''\times A_2''}[\supcast{A_1\times A_2}{A_1'\times A_2'}[x]]\\
&\equidyn\pmpairWtoXYinZ x y z \supcast{A_1'\times A_2'}{A_1''\times A_2''}[\supcast{A_1\times A_2}{A_1'\times A_2'}[(y,z)]]\tag{$\times\eta$}\\
&\equidyn\pmpairWtoXYinZ x y z \supcast{A_1'\times A_2'}{A_1''\times A_2''}[(\supcast{A_1}{A_1'}[y], \supcast{A_2}{A_2'}[z])]\tag{cast reduction}\\
&\equidyn\pmpairWtoXYinZ x y z (\supcast{A_1'}{A_1''}[\supcast{A_1}{A_1'}[y]], \supcast{A_2'}{A_2''}[\supcast{A_2}{A_2'}[z]])\tag{cast reduction}\\
&\equidyn\pmpairWtoXYinZ x y z (\supcast{A_1}{A_1''}[y], \supcast{A_2}{A_2''}[z])\tag{IH}\\
&=\supcast{A_1\times A_2}{A_1'' \times A_2''}[x]\tag{definition}
\end{align*}

* $U \u B \ltdyn U \u B' \ltdyn U \u B''$.
We need to show

\[
x : U \u B \vdash \supcast{U\u B'}{U\u B''}[\supcast{U\u B}{U\u B'}[x]] \equidyn
\supcast{U\u B}{U\u B''}[x] : U\u B''
\]

By composition of ep pairs, we know $(x.\supcast{U\u B'}{U\u
B''}[\supcast{U\u B}{U\u B'}[x]], \sdncast{\u B}{\u
B'}[\sdncast{\u B'}{\u B''}])$ is a computation ep pair.
Furthermore, by inductive hypothesis, we know

\[  \sdncast{\u B}{\u B'}[\sdncast{\u B'}{\u B''}] \equidyn \sdncast{\u B}{\u B''}\]

so then both sides form ep pairs paired with $\sdncast{\u
B}{\u B''}$, so it follows because computation projections
determine embeddings <ref>.

* $\u B \ltdyn \u B' \ltdyn \u B''$

* If $\u B = \top$, then the result is immediate by $\eta\top$.

* If $\u B = \dync$, then $\u B' = \u B'' = \dync$ then both
sides are just $\bullet$.

* If $\u B \not\in \{\dync, \top\}$, and $\u B' = \dync$, then
$\u B'' = \dync$

\[ \sdncast{\u B}{\dync}[\sdncast{\dync}{\dync}] = \sdncast{\u B}{\dync} \]

* If $\u B,\u B' \not\in \{\dync,\top\}$, and $\u B'' = \dync$ , and $\floor {\u B} = \floor {\u B'}$, which we
call $\u G$. Then we need to show

\[ \sdncast{\u B}{\u B'}[\sdncast{\u B'}{\u G}[\sdncast{\u G}{\dync}]]
\equidyn
\sdncast{\u B}{\u G}[\sdncast{\u G}[\dync]]
\]

so the result follows from the case $\u B \ltdyn \u B' \ltdyn \u
G$, which is handled below.

* If $\u B,\u B',\u B'' \not\in \{\dync, \top\}$, then they all have the
same top-level constructor:

* $\with$ We are given $\u B_1 \ltdyn \u B_1' \ltdyn \u
B_1''$ and $\u B_2 \ltdyn \u B_2' \ltdyn \u B_2''$ and we need to show

\[
\bullet : \u B_1'' \with \u B_2''
\vdash
\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\sdncast{\u B_1' \with \u B_2'}{\u B_1'' \with \u B_2''}]
: \u B_1 \with \u B_2
\]

We proceed as follows:

\begin{align*}
&\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\sdncast{\u B_1' \with \u B_2'}{\u B_1'' \with \u B_2''}]\\
&\equidyn\pairone{\pi\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\sdncast{\u B_1' \with \u B_2'}{\u B_1'' \with \u B_2''}]}\tag{$\with\eta$}\\
&\quad\pairtwo{\pi'\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\sdncast{\u B_1' \with \u B_2'}{\u B_1'' \with \u B_2''}]}\\
&\equidyn\pairone{\sdncast{\u B_1}{\u B_1'}[\pi\sdncast{\u B_1' \with \u B_2'}{\u B_1'' \with \u B_2''}]}\tag{cast reduction}\\
&\quad\pairtwo{\sdncast{\u B_2}{\u B_2'}[\pi'\sdncast{\u B_1' \with \u B_2'}{\u B_1'' \with \u B_2''}]}\\
&\equidyn\pairone{\sdncast{\u B_1}{\u B_1'}[\sdncast{\u B_1'}{\u B_1''}[\pi\bullet]]}\tag{cast reduction}\\
&\quad\pairtwo{\sdncast{\u B_2}{\u B_2'}\sdncast{\u B_2'}{\u B_2''}[\pi'\bullet]}\\
&\equidyn\pair{\sdncast{\u B_1}{\u B_1''}[\pi\bullet]}{\sdncast{\u B_2}{\u B_2''}[\pi'\bullet]}\tag{IH}\\
&= \sdncast{\u B_1 \with \u B_2}{\u B_1'' \with \u B_2''} \tag{definition}
\end{align*}

* $\to$, assume we are given $A \ltdyn A' \ltdyn A''$ and
$\u B \ltdyn \u B' \ltdyn \u B''$, then we proceed:

\begin{align*}
&\sdncast{A \to \u B}{A' \to \u B'}[\sdncast{A' \to \u B'}{A'' \to \u B''}]\\
&\equidyn \lambda x:A. (\sdncast{A \to \u B}{A' \to \u B'}[\sdncast{A' \to \u B'}{A'' \to \u B''}][\bullet])\,x\tag{$\to\eta$}\\
&\equidyn \lambda x:A. \sdncast{\u B}{\u B'}[(\sdncast{A' \to \u B'}{A'' \to \u B''}[\bullet])\, \supcast{A}{A'}[x]] \tag{cast reduction}\\
&\equidyn \lambda x:A. \sdncast{\u B}{\u B'}[\sdncast{\u B'}{\u B''}[\bullet\, \supcast{A'}{A''}[\supcast{A}{A'}[x]]]]\tag{cast reduction}\\
&\equidyn \lambda x:A. \sdncast{\u B}{\u B''}[\bullet\,\supcast{A}{A''}[x]]\\
&= \sdncast{A \to \u B}{A \to \u B''}[\bullet]\tag{definition}
\end{align*}

* $\u F A \ltdyn \u F A' \ltdyn \u F A''$. First, by
composition of ep pairs, we know

\[ (x. \supcast{A'}{A''}[\supcast{A}{A'}[x]], \sdncast{\u F
A}{\u F A'})[\sdncast{\u F A'}{\u F A''}]\]

form a value ep pair.
Furthermore, by inductive hypothesis, we know

\[ x : A \vdash \supcast{A'}{A''}[\supcast{A}{A'}[x]] \equidyn \supcast{A}{A''}[x] \]

so the two sides of our equation are both projections with the
same value embedding, so the equation follows from uniqueness
of projections from value embeddings.

The final lemma before the graduality theorem lets us “move a cast”
from left to right or vice-versa, via the adjunction property for ep

These arise in the proof cases for $\kw{return}$ and $\kw{thunk}$, because in those
cases the inductive hypothesis is in terms of an upcast (downcast) and
the conclusion is in terms of a a downcast (upcast).

For any value embedding-projection pair $V_e,S_p$ from $A$ to $A'$,
the following are equivalent:

Γ⊢V_e[V] M : F̆ A'
Γ⊢V S_p[M] : F̆ A

For any computation ep pair $(V_e,S_p)$ from $\u B$ to $\u B'$, the
following are equivalent:

Γ, z' : U B̆' ⊢M S[S_p[z']] : C̆
Γ, z : U B̆ ⊢M[V_e/z'] S[z] : C̆

* Assume $\ret V_e[V] \ltdyn M : \u F A'$. Then by retraction,
$\ret V \ltdyn S_p[\ret V_e[V]]$ so by transitivity, the result
follows by substitution:

S_p S_p V_e[V] M
S_p[V_e[V]] M

* Assume $\ret V \ltdyn S_p[M] : \u F A$. Then by projection,
$\bindXtoYinZ {S_p[M]} x \ret V_e[x] \ltdyn M$, so it is sufficient to show

\[ \ret V_e[V] \ltdyn \bindXtoYinZ {S_p[M]} x \ret V_e[x] \]

but again by substitution we have

\[ \bindXtoYinZ {\ret V} x \ret V_e[x] \ltdyn \bindXtoYinZ {S_p[M]} x \ret V_e[x]\]

and by $\u F\beta$, the LHS is equivalent to $\ret V_e[V]$.

* Assume $z' : U\u {B'} \vdash M \ltdyn S[S_p[\force z']]$, then
by projection, $S[S_p[\force V_e]] \ltdyn S[\force z]$
and by substitution:

M S[S_p[z']]V_e V_e S[S_p[V_e]] = (S[S_p[z']])[V_e/z']
M[V_e/z'] S[S_p[V_e]]

* Assume $z : U \u B \vdash M[V_e/z'] \ltdyn S[\force z]$. Then
by retraction, $M \ltdyn M[V_e[\thunk{S_p[\force z]}]]$ and by

\[ M[V_e[\thunk{S_p[\force z]}]] \ltdyn S[\force \thunk{S_p[\force z]}] \]

and the right is equivalent to $S[S_p[\force z]]$ by $U\beta$.

Finally, we prove the axiomatic graduality theorem.

In addition to the lemmas above, the main task is to prove the
“compatibility” cases which are the congruence cases for introduction
and elimination rules.

These come down to proving that the casts “commute” with
introduction/elimination forms, and are all simple calculations.
[Axiomatic Graduality]
For any dynamic type interpretation, the following are true:

Φ: ΓΓ'

Ψ: ΔΔ'

ΦΨ⊢M M' : B̆ B̆'
ΓΔ' ⊢M[Ψ] B̆B̆'[M'[Φ]] : B̆

Φ: ΓΓ'

Φ⊢V V' : A A'
Γ ⊢AA'[V] V'[Φ] : A'

By mutual induction over term dynamism derivations. For the $\beta,
\eta$ and reflexivity rules, we use the identity expansion lemma and
the corresponding $\beta, \eta$ rule of

For compatibility rules a pattern emerges.  Universal rules
(positive intro, negative elim) are easy, we don't need to reason about
casts at all. For “(co)-pattern matching rules” (positive elim,
negative intro), we need to invoke the $\eta$ principle (or
commuting conversion, which is derived from the $\eta$ principle).
In all compatibility cases, the cast reduction lemma keeps the
proof straightforward.

Fortunately, all reasoning about “shifted” casts is handled in
lemmas, and here we only deal with the “nice” value upcasts/stack

* Transitivity for values: The GTT rule is

\[
\inferrule{
\Phi : \Gamma \ltdyn \Gamma' \and \Phi' : \Gamma' \ltdyn \Gamma'' \and
\Phi'' : \Gamma \ltdyn \Gamma''
\\
\Phi \vdash V \ltdyn V' : A \ltdyn A'\\
\Phi' \vdash V' \ltdyn V'' : A' \ltdyn A''\\
{ \Phi'' \vdash V \ltdyn V'' : A \ltdyn A''}
\]

Which under translation (and the same assumptions about the contexts) is

\[
\inferrule
{\sem{\Gamma} \vdash \supcast{A}{A'}[\sem{V}] \ltdyn \sem{V'}[\sem{\Phi}] : \sem{A'}\\
\sem{\Gamma'} \vdash \supcast{A'}{A'}[\sem{V'}] \ltdyn \sem{V''}[\sem{\Phi'}] : \sem{A''}
{\sem{\Gamma} \vdash \supcast{A}{A''}[\sem{V}] \ltdyn \sem{V''}[\sem{\Phi''}] : \sem{A''}}
\]

We proceed as follows, the key lemma here is the cast decomposition lemma:

\begin{align*}
\supcast{A}{A''}[\sem{V}]
\supcast{A'}{A''}[\supcast{A}{A'}[\sem{V}]] \tag{cast decomposition}\\
&\ltdyn \supcast{A'}{A''}[\sem{V'}[\sem{\Phi}]] \tag{IH}\\
&\ltdyn \sem{V''}[\sem{\Phi'}][\sem{\Phi}] \tag{IH}\\
&\equidyn \sem{V''}[\sem{\Phi''}] \tag{cast decomposition}
\end{align*}

* Transitivity for terms:
The GTT rule is

\[
\inferrule{
\Phi : \Gamma \ltdyn \Gamma' \and \Phi' : \Gamma' \ltdyn \Gamma'' \and
\Phi'' : \Gamma \ltdyn \Gamma''
\and \Psi : \Delta \ltdyn \Delta' \and \Psi : \Delta' \ltdyn \Delta''
\and \Psi'' : \Delta\ltdyn \Delta''
\\
\Phi \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'\\
\Phi' \pipe \Psi' \vdash M' \ltdyn M'' : \u B' \ltdyn \u B''\\
{ \Phi'' \pipe \Psi'' \vdash M \ltdyn M'' : \u B \ltdyn \u B''}
\]

Which under translation (and the same assumptions about the contexts) is

\[
\inferrule
{\sem{\Gamma} \pipe \sem{\Delta'} \vdash \sem{M}[\sem{\Psi}] \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}]] : \sem{\u B}\\
\sem{\Gamma'} \pipe \sem{\Delta''} \vdash \sem{M'}[\sem{\Psi'}] \ltdyn \sdncast{\u B'}{\u B''}[\sem{M''}[\sem{\Phi'}]] : \sem{\u B'}}
{\sem{\Gamma} \pipe \sem{\Delta''} \vdash \sem{M}[\sem{\Psi''}] \ltdyn \sdncast{\u B}{\u B''}[\sem{M''}[\sem{\Phi''}]] : \sem{\u B}}
\]

We proceed as follows, the key lemma here is the cast decomposition lemma:

\begin{align*}
\sem{M}[\sem{\Psi''}]
\sem{M}[\sem{\Psi}][\sem{\Psi'}] \tag{Cast decomposition}\\
&\ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Psi'}][\sem{\Phi}]]\tag{IH}\\
&\ltdyn \sdncast{\u B}{\u B'}[\sdncast{\u B'}{\u B''}[\sem{M''}[\sem{\Phi'}][\sem{\Phi}]]]\tag{IH}\\
&\equidyn \sdncast{\u B}{\u B''}[\sem{M''}[\sem{\Phi''}]] \tag{Cast decomposition}
\end{align*}

* Substitution of a value in a value:
The GTT rule is

\[
\inferrule
{\Phi, x \ltdyn x' : A_1 \ltdyn A_1' \vdash V_2 \ltdyn V_2' : A_2 \ltdyn A_2'\\
\Phi \vdash V_1 \ltdyn V_1' : A_1 \ltdyn A_1'}
{\Phi \vdash V_2[V_1/x]\ltdyn V_2'[V_1'/x'] : A_2 \ltdyn A_2'}
\]

Where $\Phi : \Gamma \ltdyn \Gamma'$. Under translation, we need to show

\[
\inferrule
{\sem\Gamma, x : \sem{A_1} \vdash \supcast{A_2}{A_2'}[\sem{V_2}] \ltdyn \sem{V_2'}[\sem\Phi][\supcast{A_1}{A_1'}[x]/x'] : \sem{A_2'}\\
\sem\Gamma \vdash \supcast{A_1}{A_1'}[\sem{V_1}] \ltdyn \sem{V_1'}[\sem\Phi] : \sem{A_1'}}
{\sem\Gamma \vdash \supcast{A_2}{A_2'}[\sem{V_2[V_1/x]}] \ltdyn \sem{V_2'[V_1'/x']}[\sem\Phi] : \sem{A_2'}}
\]

Which follows by compositionality:

\begin{align*}
\supcast{A_2}{A_2'}[\sem{V_2[V_1/x]}]
&= (\supcast{A_2}{A_2'}[\sem{V_2}])[\sem{V_1}/x] \tag{Compositionality}\\
&\ltdyn \sem{V_2'}[\sem\Phi][\supcast{A_1}{A_1'}[x]/x'][\sem{V_1}/x]\tag{IH}\\
&= \sem{V_2'}[\sem\Phi][\supcast{A_1}{A_1'}[\sem{V_1}]/x']\\
&\ltdyn \sem{V_2'}[\sem\Phi][\sem{V_1'}[\sem\Phi]/x']\tag{IH}\\
&= \sem{V_2'[V_1'/x']}[\sem\Phi]
\end{align*}

* Substitution of a value in a term:
The GTT rule is

\[
\inferrule
{\Phi, x \ltdyn x' : A \ltdyn A' \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'\\
\Phi \vdash V \ltdyn V' : A \ltdyn A'
{\Phi \vdash M[V/x] \ltdyn M'[V'/x'] : \u B \ltdyn \u B'}
\]

Where $\Phi : \Gamma \ltdyn \Gamma'$ and $\Psi : \Delta \ltdyn \Delta'$.
Under translation this is:

\[
\inferrule
{\sem\Gamma, x : \sem{A} \pipe \sem\Delta \vdash \sem M \ltdyn \sdncast{\u B}{\u B'}[\sem {M'}[\sem\Phi][\supcast{A}{A'}[x]/x']] : \sem{\u B}\\
\sem\Gamma \vdash \supcast{A}{A'}[{\sem V}] \ltdyn \sem{V'}[\sem\Phi] : \sem{A'}}
{\sem\Gamma \pipe \sem\Delta \vdash \sem {M[V/x]} \ltdyn \sdncast{\u B}{\u B'}[\sem{M'[V'/x']}[\sem\Phi]] : \sem{\u B}}
\]

Which follows from compositionality of the translation:

\begin{align*}
\sem {M[V/x]}
&= \sem{M}[\sem{V}/x] \tag{Compositionality}\\
&\ltdyn \sdncast{\u B}{\u B'}[\sem {M'}[\sem\Phi][\supcast{A}{A'}[x]/x']][\sem{V}/x] \tag{IH}\\
&= \sdncast{\u B}{\u B'}[\sem {M'}[\sem\Phi][\supcast{A}{A'}[\sem{V}]/x']]\\
&\ltdyn \sdncast{\u B}{\u B'}[\sem {M'}[\sem\Phi][\sem{V'}[\sem\Phi]/x']]\tag{IH}\\
&= \sdncast{\u B}{\u B'}[\sem{M'[V'/x']}[\sem\Phi]] \tag{Compositionality}
\end{align*}

* Substitution of a term in a stack:
The GTT rule is

\[
\inferrule
{\Phi \pipe \bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash S \ltdyn S' : \u C \ltdyn \u C'\\
\Phi \pipe \cdot \vdash M \ltdyn M' : \u B \ltdyn \u B'}
{\Phi \pipe \cdot \vdash S[M]\ltdyn S'[M'] : \u C \ltdyn \u C'}
\]

Where $\Phi : \Gamma \ltdyn \Gamma'$.
Under translation this is

\[
\inferrule
{\sem\Gamma \pipe \bullet : \sem{\u B'} \vdash \sem{S}[\sdncast{\u B}{\u B'}[\bullet]] \ltdyn \sdncast{\u C}{\u C'}[\sem{S'}[\sem\Phi]] : \sem{\u C}\\
\sem\Gamma \pipe \cdot \vdash \sem{M} \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]] : \sem{\u B}}
{\sem\Gamma \pipe \cdot \vdash \sem{S[M]} \ltdyn \sdncast{\u C}{\u C'}[\sem{S'[M']}[\sem\Phi]] : \sem{\u C}}
\]

We follows easily using compositionality of the translation:

\begin{align*}
\sem{S[M]}
&= \sem{S}[\sem{M}] \tag{Compositionality}\\
&\ltdyn   \sem{S}[\sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]] \tag{IH}\\
&\ltdyn   \sdncast{\u C}{\u C'}[\sem{S'}[\sem\Phi][\sem{M'}[\sem\Phi]]]\tag{IH}\\
&= \sdncast{\u C}{\u C'}[\sem{S'[M']}[\sem\Phi]] \tag{Compositionality}
\end{align*}

* Variables: The GTT rule is

\[ \Gamma_1 \ltdyn \Gamma_1' ,x \ltdyn x' : A \ltdyn A', \Gamma_2 \ltdyn \Gamma_2' \vdash x \ltdyn x' : A \ltdyn A' \]

which under translation is

\[ \sem{\Gamma_1}, x : \sem A, \sem{\Gamma_2} \vdash \supcast{A}{A'}[x] \ltdyn \supcast{A}{A'}[x] : \sem{A'} \]

which is an instance of reflexivity.

* Hole: The GTT rule is

\[ \Phi \pipe \bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn \bullet : \u B \ltdyn \u B' \]

which under translation is

\[ \sem\Gamma \pipe \bullet : \u B' \vdash \sdncast{\u B}{\u B'}[\bullet] \ltdyn \sdncast{\u B}{\u B'}[\bullet] : \u B \]

which is an instance of reflexivity.

* Error is bottom: The GTT axiom is

\[ \Phi \vdash \err \ltdyn M : \u B \]

where $\Phi : \Gamma \ltdyn \Gamma'$, so we need to show

\[ \sem\Gamma \vdash \err \ltdyn \sdncast{\u B}{\u B}[\sem{M}[\sem{\Phi}]] : \sem{\u B} \]

which is an instance of the error is bottom axiom of CBPV.

* Error strictness: The GTT axiom is

\[
\Phi \vdash S[\err] \ltdyn \err : \u B
\]

where $\Phi : \Gamma \ltdyn \Gamma'$, which under translation is

\[
\sem\Gamma \vdash \sem{S}[\err] \ltdyn \sdncast{\u B}{\u B}[\err] : \sem{\u B}
\]

By strictness of stacks in CBPV, both sides are equivalent to
$\err$, so it follows by reflexivity.

* UpCast-L: The GTT axiom is

\[
x \ltdyn x' : A \ltdyn A' \vdash \upcast{A}{A'}x \ltdyn x' : A'
\]

which under translation is

\[
x : \sem{A} \vdash \supcast{A'}{A'}[\supcast{A}{A'}[x]] \ltdyn \supcast{A}{A'}[x] : A'
\]

Which follows by identity expansion and reflexivity.

* UpCast-R: The GTT axiom is

\[
x : A \vdash x \ltdyn \upcast{A}{A'}x : A \ltdyn A'
\]

which under translation is

\[
x : \sem{A} \vdash \supcast{A}{A'}[x] \ltdyn \supcast{A}{A'}[\supcast{A}{A}[x]] : \sem{A'}
\]

which follows by identity expansion and reflexivity.

* DnCast-R: The GTT axiom is

\[
\bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn \dncast{\u B}{\u B'} : \u B
\]

Which under translation is

\[
\bullet : \sem{\u B'} \vdash
\sdncast{\u B}{\u B'}[\bullet]
\ltdyn
\sdncast{\u B}{\u B}[\sdncast{\u B}{\u B'}[\bullet]]
: \sem{\u B}
\]

Which follows by identity expansion and reflexivity.

* DnCast-L: The GTT axiom is

\[
\bullet : \u B' \vdash \dncast{\u B}{\u B'} \bullet \ltdyn \bullet : \u B \ltdyn \u B'
\]

So under translation we need to show

\[
\bullet : \sem{\u B'} \vdash
\sdncast{\u B}{\u B'}[\sdncast{\u B'}{\u B'}[\bullet]]
\ltdyn
\sdncast{\u B}{\u B'}\bullet : \sem{\u B}
\]

Which follows immediately by reflexivity and the lemma that
identity casts are identities.

* $0$ elim, we do the term case, the value case is similar

\[
\inferrule
{\upcast{0}{0}[\sem{V}] \ltdyn \sem{V'}[\sem\Phi]}
{\absurd \sem{V} \ltdyn \dncast{\u B}{\u B'}\absurd\sem{V'}[\sem\Phi]}
\]

Immediate by $0\eta$.

* $+$ intro, we do the $\inl$ case, the $\inr$ case is the same:

\[
\inferrule
{\supcast{A_1}{A_1'}[\sem{V}]\ltdyn \sem{V'}[\sem\Phi]}
{\supcast{A_1+A_2}{A_1'+A_2'}[\inl\sem{V}]\ltdyn \inl\sem{V'}[\sem\Phi]}
\]

Which follows easily:

\begin{align*}
\supcast{A_1+A_2}{A_1'+A_2'}[\inl\sem{V}]
&\equidyn \inl \supcast{A_1}{A_1'}\sem{V}\tag{cast reduction}\\
&\ltdyn \inl \sem{V'}[\sem\Phi]\tag{IH}
\end{align*}

* $+$ elim, we do just the cases where the continuations are terms:

\[
\inferrule
{\supcast{A_1 + A_2}{A_1' + A_2'}[\sem{V}] \ltdyn \sem{V'}[\sem\Phi]\\
\sem{M_1}[\sem\Psi] \ltdyn \sem{M_1'}[\sem\Phi][\supcast{A_1}{A_1'}[x_1]/x_1']\\
\sem{M_2}[\sem\Psi] \ltdyn \sem{M_2'}[\sem\Phi][\supcast{A_2}{A_2'}[x_2]/x_2']}
{\caseofXthenYelseZ {\sem V} {x_1. \sem{M_1}[\sem\Psi]}{x_2. \sem{M_2}[\sem\Psi]} \ltdyn \sdncast{\u B}{\u B'}[\caseofXthenYelseZ {\sem V'[\sem\Phi]} {x_1'. \sem{M_1'}[\sem\Phi]}{x_2'. \sem{M_2'}[\sem\Phi]}]}
\]

\begin{align*}
& \caseofXthenYelseZ {\sem V} {x_1. \sem{M_1}[\sem\Psi]}{x_2. \sem{M_2}[\sem\Psi]}\\
\sdncast{\u B}{\u B'}[\caseofXthenYelseZ {\sem V} {x_1. \sem{M_1'}[\sem\Phi][\supcast{A_1}{A_1'}[x_1]/x_1']}{x_2. \sem{M_2'}[\sem\Phi][\supcast{A_2}{A_2'}[x_2]/x_2']}]\tag{IH}\\
\caseofX {\sem V}\tag{comm conv}\\
&\qquad\thenY{x_1. \sdncast{\u B}{\u B'}[\sem{M_1'}[\sem\Phi][\supcast{A_1}{A_1'}[x_1]/x_1']]}\\
&\qquad\elseZ{x_2. \sdncast{\u B}{\u B'}[\sem{M_2'}[\sem\Phi][\supcast{A_2}{A_2'}[x_2]/x_2']]}\\
\caseofX {\sem V}\tag{$+\beta$}\\
&\qquad\thenY{x_1. \sdncast{\u B}{\u B'}[\caseofXthenYelseZ {\inl \supcast{A_1}{A_1'}x_1} {x_1'. \sem{M_1'}[\sem\Phi]}{x_2'. \sem{M_2'}[\sem\Phi]}]}\\
&\qquad\elseZ{x_2. \sdncast{\u B}{\u B'}[\caseofXthenYelseZ {\inr \supcast{A_2}{A_2'}x_2} {x_1'. \sem{M_1'}[\sem\Phi]}{x_2'. \sem{M_2'}[\sem\Phi]}]}\\
\caseofX {\sem V}\tag{cast reduction}\\
&\qquad\thenY{x_1. \sdncast{\u B}{\u B'}[\caseofXthenYelseZ {\supcast{A_1+A_2}{A_1'+A_2'}\inl x_1} {x_1'. \sem{M_1'}[\sem\Phi]}{x_2'. \sem{M_2'}[\sem\Phi]}]}\\
&\qquad\elseZ{x_2. \sdncast{\u B}{\u B'}[\caseofXthenYelseZ {\supcast{A_1+A_2}{A_1'+A_2'}\inr x_2} {x_1'. \sem{M_1'}[\sem\Phi]}{x_2'. \sem{M_2'}[\sem\Phi]}]}\\
\sdncast{\u B}{\u B'}[\caseofXthenYelseZ {\supcast{A_1+A_2}{A_1'+A_2'}[\sem V]} {x_1'. \sem{M_1'}[\sem\Phi]}{x_2'. \sem{M_2'}[\sem\Phi]}]\\
\sdncast{\u B}{\u B'}[\caseofXthenYelseZ {\sem{V'}[\sem\Phi]} {x_1'. \sem{M_1'}[\sem\Phi]}{x_2'. \sem{M_2'}[\sem\Phi]}]\tag{IH}\\
\end{align*}

* $1$ intro:

\[
\inferrule
{\supcast{1}{1}[()]\ltdyn ()}
\]

Immediate by cast reduction.

* $1$ elim (continuations are terms case):

\[
\inferrule
{\supcast{1}{1}[\sem{V}] \ltdyn \sem{V'}[\sem\Phi]\\
\sem{M}[\sem\Psi] \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]
{\pmpairWtoinZ {\sem V} {\sem{M}[\sem{\Psi}]}
\ltdyn
\dncast{\u B}{\u B'}[\pmpairWtoinZ {\sem V'[\sem\Phi]} {\sem{M'}[\sem{\Phi}]}]}
\]

which follows by identity expansion <ref>.

* $\times$ intro:

\[
\inferrule
{\supcast{A_1}{A_1'}{\sem{V_1}} \ltdyn \sem{V_1'[\sem\Phi]}\\
\supcast{A_2}{A_2'}{\sem{V_2}} \ltdyn \sem{V_2'[\sem\Phi]}}
{\supcast{A_1 \times A_2}{A_1' \times A_2'}[(\sem{V_1},\sem{V_2})]
\ltdyn
(\sem{V_1'[\sem\Phi]}, \sem{V_2'[\sem\Phi]})}
\]

We proceed:

\begin{align*}
\supcast{A_1 \times A_2}{A_1' \times A_2'}[(\sem{V_1},\sem{V_2})]
(\supcast{A_1}{A_1'}{\sem{V_1}},\supcast{A_2}{A_2'}{\sem{V_2}})\tag{cast reduction}\\
&\ltdyn (\sem{V_1'[\sem\Phi]}, \sem{V_2'[\sem\Phi]}) \tag{IH}
\end{align*}

* $\times$ elim: We show the case where the continuations are
terms, the value continuations are no different:

\[
\inferrule
{\supcast{A_1\times A_2}{A_1' \times A_2'}[\sem{V}] \ltdyn \sem{V'}[\sem\Phi]\\
\sem{M}[\sem\Psi] \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi][\supcast{A_1}{A_1'}[x]/x'][\supcast{A_2}{A_2'}[y]/y']]
{\pmpairWtoXYinZ {\sem V} x y {\sem{M}[\sem{\Psi}]}
\ltdyn
\dncast{\u B}{\u B'}[\pmpairWtoXYinZ {\sem V'[\sem\Phi]} {x'} {y'} {\sem{M'}[\sem{\Phi}]}]
\]

We proceed as follows:

\begin{align*}
&\pmpairWtoXYinZ {\sem V} x y {\sem{M}[\sem{\Psi}]}\\
&\ltdyn\pmpairWtoXYinZ {\sem V} x y \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi][\supcast{A_1}{A_1'}[x]/x'][\supcast{A_2}{A_2'}[y]/y']]\tag{IH}\\
\pmpairWtoXYinZ {\sem V} x y\tag{$\times\beta$}\\
&\qquad \pmpairWtoXYinZ {(\supcast{A_1}{A_1'}[x],\supcast{A_2}{A_2'}[y])} {x'} {y'} \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]\\
\pmpairWtoXYinZ {\sem V} x y\tag{cast reduction}\\
&\qquad \pmpairWtoXYinZ {\supcast{A_1\times A_2'}{A_1'\times A_2'}[(x,y)]} {x'} {y'} \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]\\
\pmpairWtoXYinZ {\supcast{A_1\times A_2}{A_1'\times A_2'}[{\sem V}]} {x'} {y'} \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]\tag{$\times\eta$}\\
&\ltdyn \pmpairWtoXYinZ {\sem{V'}[\sem\Phi]} {x'}{y'} \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]\tag{IH}\\
&\equidyn \sdncast{\u B}{\u B'}[\pmpairWtoXYinZ {\sem{V'}[\sem\Phi]} {x'}{y'}\sem{M'}[\sem\Phi]]\tag{commuting conversion}
\end{align*}

* $U$ intro:

\[
\inferrule
{\sem{M} \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]}
{\supcast{U\u B}{U \u B'}[\thunk\sem{M}] \ltdyn \thunk\sem{M'}[\sem\Phi]}
\]

We proceed as follows:

\begin{align*}
\supcast{U\u B}{U \u B'}[\thunk\sem{M}]
&\ltdyn \supcast{U\u B}{U \u B'}[\thunk\sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]]\tag{IH}\\
&\ltdyn \thunk \sem{M'}[\sem\Phi]\tag{alt projection}
\end{align*}

* $U$ elim:

\[
\inferrule
{\supcast{U \u B}{U \u B'}[\sem{V}] \ltdyn \sem{V'}[\sem\Phi]}
{\force \sem V \ltdyn \sdncast{\u B}{\u B'}\force \sem {V'}[\sem\Phi]}
\]

By hom-set formulation of adjunction <ref>.

* $\top$ intro:

\[
\inferrule{}{\{\} \ltdyn \sdncast{\top}{\top}[\{\}]}
\]

Immediate by $\top\eta$

* $\with$ intro:

\[
\inferrule
{\sem{M_1}[\sem{\Psi}]\ltdyn \sdncast{\u B_1}{\u B_1'}[\sem{M_1'}[\sem{\Phi}]]\\
\sem{M_2}[\sem{\Psi}]\ltdyn \sdncast{\u B_2}{\u B_2'}[\sem{M_2'}[\sem{\Phi}]]}
\ltdyn
\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\pair{\sem{M_1'}[\sem{\Phi}]}{\sem{M_2'}[\sem{\Phi}]}]}
\]

We proceed as follows:

\begin{align*}
\pair{\sdncast{\u B_1}{\u B_1'}[\sem{M_1'}[\sem{\Phi}]]}{\sdncast{\u B_2}{\u B_2'}[\sem{M_2'}[\sem{\Phi}]]}\tag{IH}\\
\pairone{\pi\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\pair{\sem{M_1'}[\sem{\Phi}]}{\sem{M_2'}[\sem{\Phi}]}]}\tag{cast reduction}\\
&\quad \pairtwo{\pi'\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\pair{\sem{M_1'}[\sem{\Phi}]}{\sem{M_2'}[\sem{\Phi}]}]}\\
\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\pair{\sem{M_1'}[\sem{\Phi}]}{\sem{M_2'}[\sem{\Phi}]}]\tag{$\with\eta$}
\end{align*}

* $\with$ elim, we show the $\pi$ case, $\pi'$ is symmetric:

\[
\inferrule
{\sem{M}[\sem{\Psi}] \ltdyn \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\sem{M'}[\sem{\Phi}]]}
{\pi\sem{M}[\sem{\Psi}] \ltdyn \sdncast{\u B_1}{\u B_1'}[\pi\sem{M'}[\sem{\Phi}]]}
\]

We proceed as follows:

\begin{align*}
\pi\sem{M}[\sem{\Psi}]
&\ltdyn \pi \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\sem{M'}[\sem{\Phi}]]\tag{IH}\\
\sdncast{\u B_1}{\u B_1'}[\pi\sem{M'}[\sem{\Phi}]]\tag{cast reduction}
\end{align*}

\[
\inferrule
{\sem{M}[\sem{\Psi}] \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}][\supcast{A}{A'}{x}/x']]}
{\lambda x:A. \sem{M}[\sem{\Psi}] \ltdyn \sdncast{A \to \u B}{A'\to\u B'}[\lambda x':A'. \sem{M'}[\sem{\Phi}]]}
\]

We proceed as follows:

\begin{align*}
&\lambda x:A. \sem{M}[\sem{\Psi}]\\
\lambda x:A. \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}][\supcast{A}{A'}{x}/x']]\tag{IH}\\
\lambda x:A. (\sdncast{A \to \u B}{A' \to \u B'}[\lambda x'. \sem{M'}[\sem{\Phi}]])\, x\tag{cast reduction}\\
\sdncast{A \to \u B}{A' \to \u B'}[\lambda x'. \sem{M'}[\sem{\Phi}]]\tag{$\to\eta$}
\end{align*}

* We need to show

\[
\inferrule
{\sem{M}[\sem{\Psi}] \ltdyn \sdncast{A \to \u B}{A' \to \u B'}[\sem{M'}[\sem{\Phi}]]\\
\supcast{A}{A'}[\sem{V}] \ltdyn \sem{V'}[\sem{\Phi}]}
{\sem{M}[\sem{\Psi}]\,\sem{V} \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}]\, \sem{V'}[\sem{\Phi}]]}
\]

We proceed:

\begin{align*}
(\sdncast{A \to \u B}{A' \to \u B'}[\sem{M'}[\sem{\Phi}]])\,\sem{V}\tag{IH}\\
\sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}]\,(\supcast{A}{A'}{\sem{V}})]\tag{cast reduction}\\
\sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}]\,\sem{V'}[\sem{\Phi}]] \tag{IH}
\end{align*}

* We need to show

\[
\inferrule
{\supcast{A}{A'}[\sem{V}] \ltdyn \sem{V'}[\sem{\Phi}]}
{\ret\sem{V}\ltdyn \sdncast{\u F A}{\u FA'}[\ret\sem{V'}[\sem{\Phi}]]}
\]

By hom-set definition of adjunction <ref>

* We need to show

\[
\inferrule
{\sem{M}[\sem{\Psi}] \ltdyn \sdncast{\u F A}{\u F A'}[\sem{M'}[\Phi]]\\
\sem{N} \ltdyn \sdncast{\u B}{\u B'}[\sem{N}[\Phi][\supcast{A}{A'} x/x']]}
{\bindXtoYinZ {\sem{M}[\sem{\Psi}]} x {\sem{N}}
\ltdyn
\sdncast{\u B}{\u B'}[{\bindXtoYinZ {\sem{M'}[\sem{\Phi}]} {x'} {\sem{N'}[\sem{\Phi}]}}]}
\]

We proceed:

\begin{align*}
&\bindXtoYinZ {\sem{M}[\sem{\Psi}]} x {\sem{N}}\\
&\ltdyn \bindXtoYinZ {\sdncast{\u F A}{\u F A'}[\sem{M'}[\Phi]]} x \sdncast{\u B}{\u B'}[\sem{N}[\Phi][\supcast{A}{A'} x/x']] \tag{IH, congruence}\\
\bindXtoYinZ {\sdncast{\u F A}{\u F A'}[\sem{M'}[\Phi]]} x\\
&\qquad \bindXtoYinZ {\ret\supcast{A}{A'}[x]} {x'}
\sdncast{\u B}{\u B'}[\sem{N}[\Phi]] \tag{$\u F\beta$}\\
& \ltdyn \bindXtoYinZ {\sem{M'}[\Phi]} {x'} \sdncast{\u B}{\u B'}[\sem{N}[\Phi]] \tag{Projection}\\
& \equidyn  \sdncast{\u B}{\u B'}[\bindXtoYinZ {\sem{M'}[\Phi]} {x'} \sem{N}[\Phi]] \tag{commuting conversion}
\end{align*}

As a corollary, we have the following conservativity result, which says
that the homogeneous term dynamisms in GTT are sound and complete for
inequalities in .

If $\Gamma \mid \Delta \vdash E, E' : T$ are two terms of the same
type in the intersection of GTT and , then $\Gamma \mid
\Delta \vdash E \ltdyn E' : T$ is provable in GTT iff it is
provable in .

The reverse direction holds because  is a syntactic subset of
GTT. The forward direction holds by axiomatic graduality and the
fact that identity casts are identities.

§ COMPLEX VALUE/STACK ELIMINATION

Next, to bridge the gap between the semantic notion of complex value
and stack with the more rigid operational notion, we perform a
complexity-elimination pass.

This translates a computation with complex values in it to an equivalent
computation without complex values: i.e., all pattern matches take place
in computations, rather than in values, and translates a term dynamism
derivation that uses complex stacks to one that uses only “simple”
stacks without pattern-matching and computation introduction forms.

Stacks do not appear anywhere in the grammar of terms, but they are
used in the equational theory (computation $\eta$ rules and error

This translation clarifies the behavioral meaning of complex values and
stacks, following <cit.>, and therefore of upcasts and downcasts.

This is related to completeness of focusing: it moves inversion rules
outside of focus phases.

The syntax of operational CBPV is as in
Figure <ref> (unshaded), but with recursive
types added as in Section <ref>, and with values and stacks

as in Figure <ref>.

A         X |μX.A |U B̆ |0 |A_1 + A_2 |1 |A_1 ×A_2

B̆      ::=     Y̆|νY̆. B̆ |F̆ A |⊤|B̆_1 B̆_2 |A →B̆

Γ    ::=     ·|Γ, x : A

Δ    ::=     ·|∙: B̆

V      ::=     x |μX.AV |V |V |() |(V_1,V_2)|M

M     ::=     _B̆ |V x M |V x M |νY̆.B̆ M |M |V |

V x_1. M_1x_2.M_2 |V M |V x y M
|V |

V |MxN |λx:A.M |M V ||M_1M_2 |πM |π' M

S     ::=     ∙|S x M |S  V |πS |π' S |νY̆.B̆S

Operational CBPV Syntax

In , values include only introduction forms, as usual for values in
operational semantics, and  stacks consist only of elimination
forms for computation types
(the syntax of  enforces an A-normal
form, where only values can be pattern-matched on, so $\kw{case}$ and
$\kw{split}$ are not evaluation contexts in the operational semantics).

Γ,x : A,Γ' ⊢x x : A

Γ∙: B̆ ⊢∙∙: B̆

Γ⊢: B̆

Γ⊢V V' : A Γ, x : A ⊢M M' : B̆

Γ⊢V x M V' x M' : B̆

Γ⊢V V' : 0
Γ⊢V V' : B̆

Γ⊢V V' : A_1
Γ⊢V V' : A_1 + A_2

Γ⊢V V' : A_2
Γ⊢V V' : A_1 + A_2

Γ⊢V V' : A_1 + A_2Γ, x_1 : A_1 ⊢M_1 M_1' : B̆Γ, x_2 : A_2 ⊢M_2 M_2' : B̆

Γ⊢V x_1. M_1x_2.M_2 V' x_1. M_1'x_2.M_2' : B̆

Γ⊢() () : 1

Γ⊢V_1 V_1' : A_1Γ⊢V_2 V_2' : A_2
Γ⊢(V_1,V_2) (V_1',V_2') : A_1 ×A_2

Γ⊢V V' : A_1 ×A_2Γ, x : A_1,y : A_2 ⊢M M' : B̆

Γ⊢V x y M V' x y M' : B̆

Γ⊢V V' : A[μX.A/X]
Γ⊢μX.A V μX.A V' : μX.A

Γ⊢V V' : μX. AΓ, x : A[μX. A/X] ⊢M M' : B̆
Γ⊢V x M V' x M' : B̆

Γ⊢M M' : B̆
Γ⊢M M' : U B̆

Γ⊢V V' : U B̆
Γ⊢V V' : B̆

Γ⊢V V' : A
Γ⊢V V' : F̆ A

Γ⊢M M' : F̆ AΓ, x: A ⊢N N' : B̆
Γ⊢M x N M' x N' : B̆

Γ, x: A ⊢M M' : B̆
Γ⊢λx : A . M λx:A. M' : A →B̆

Γ⊢M M' : A →B̆Γ⊢V V' : A
Γ⊢M V M' V' : B̆

Γ⊢M_1 M_1' : B̆_1Γ⊢M_2 M_2' : B̆_2
Γ⊢M_1 M_2 M_1' M_2' : B̆_1 B̆_2

Γ⊢M M' : B̆_1 B̆_2
Γ⊢πM πM' : B̆_1

Γ⊢M M' : B̆_1 B̆_2
Γ⊢π' M π' M' : B̆_2

Γ⊢M M' : B̆[νY̆. B̆/Y̆]
Γ⊢νY̆. B̆ M νY̆. B̆ M' : νY̆. B̆

Γ⊢M M' : νY̆. B̆
Γ⊢M M' : B̆[νY̆. B̆/Y̆]

CBPV Inequational Theory (Congruence Rules)

Vx_1. M_1x_2. M_2 M_1[V/x_1]

Vx_1. M_1x_2. M_2 M_2[V/x_2]

Γ, x : A_1 + A_2 ⊢M : B̆
Γ, x : A_1 + A_2 ⊢M x x_1. M[x_1/x]x_2. M[x_2/x] : B̆

(V_1,V_2)x_1x_2M M[V_1/x_1,V_2/x_2]

Γ, x : A_1 ×A_2 ⊢M : B̆
Γ, x : A_1 ×A_2 ⊢M x x_1x_2 M[(x_1,x_2)/x] : B̆

Γ, x : 1 ⊢M : B̆
Γ, x : 1 ⊢M M[()/x] : B̆

A VxM M[V/x]

Γ, x : μX. A ⊢M :B̆
Γ, x : μX. A ⊢M xyM[μX.A y/x] : B̆

M M

Γ⊢V : U B̆
Γ⊢V V : U B̆

V x M M[V/x]

V x M M[V/x]

Γ∙: F̆ A ⊢∙∙x x : F̆ A

(λx:A. M) V M[V/x]

Γ⊢M : A →B̆
Γ⊢M λx:A. M x : A →B̆

πMM' M

π' MM' M'

Γ⊢M : B̆_1 B̆_2
Γ⊢M πMπ' M : B̆_1 B̆_2

Γ⊢M : ⊤
Γ⊢M {} : ⊤

B̆ M M

Γ⊢M : νY̆. B̆
Γ⊢M νY̆.B̆M : νY̆. B̆

CBPV $\beta, \eta$ rules

Γ⊢M : B̆

Γ⊢S[] : B̆

Γ⊢M M : B̆

Γ⊢V V : A

ΓB̆ ⊢S S : B̆'

Γ⊢M_1 M_2 : B̆ Γ⊢M_2 M_3 : B̆
Γ⊢M_1 M_3 : B̆

Γ⊢V_1 V_2 : A Γ⊢V_2 V_3 : A
Γ⊢V_1 V_3 : A

ΓB̆ ⊢S_1 S_2 : B̆' ΓB̆ ⊢S_2 S_3 : B̆'
ΓB̆ ⊢S_1 S_3 : B̆'

Γ, x : A ⊢M_1 M_2 : B̆ Γ⊢V_1 V_2 : A
Γ⊢M_1[V_1/x] M_2[V_2/x] : B̆

Γ, x : A ⊢V_1' V_2' : A' Γ⊢V_1 V_2 : A
Γ⊢V_1'[V_1/x] V_2'[V_2/x] : A'

Γ, x : A B̆ ⊢S_1 S_2 : B̆' Γ⊢V_1 V_2 : A
ΓB̆ ⊢S_1[V_1/x] S_2[V_2/x] : B̆'

ΓB̆ ⊢S_1 S_2 : B̆' Γ⊢M_1 M_2 : B̆
Γ⊢S_1[M_1] S_2[M_2] : B̆'

ΓB̆' ⊢S_1' S_2' : B̆” ΓB̆ ⊢S_1 S_2 : B̆'
ΓB̆ ⊢S_1'[S_1] S_2'[S_2] : B̆”

CBPV logical and error rules

<cit.> translates  to , but not does not prove
the inequality preservation that we require here, so we give
alternative translation for which this property is easy to
verify (see the extended version for full details).
We translate both complex values and complex
stacks to fully general computations, so that computation
pattern-matching can replace the pattern-matching in complex values/stacks.

For example, for a closed value, we could “evaluate away”
the complexity and get a closed simple value (if we don't use $U$), but
for open terms, evaluation will get “stuck” if we pattern match on
a variable—so not every complex value can be translated to a value in

More formally, we translate a  complex value $V : A$ to a
computation $\simp{V} : \u F A$ that in  is equivalent
to $\ret V$.

Similarly, we translate a  complex stack $S$ with hole
$\bullet : \u B$ to a   computation $\simp{S}$ with a free
variable $z : U \u B$ such that in , $\simp S \equidyn
S[\force z]$.

Computations $M : \u B$ are translated to computations $\simp{M}$ with
the same type.

The de-complexification procedure is defined as follows.

We note that this translation is not the one presented in
<cit.>, but rather a more inefficient version that, in CPS
terminology, introduces many administrative redices.

Since we are only proving results up to observational equivalence
anyway, the difference doesn't change any of our theorems, and makes
some of the proofs simpler.

We define

∙   =    z

x    =    x

V    =     V x x

M  V     =    V x M  x

V    =    V x x

V    =    V x x

V x_1. E_1x_2. E_2    =
V x x x_1. E_1x_2. E_2

V E    =
V w w E

V x y E    =
V w w x y E

V x E    =    V y y x E

V    =    V x x

V    =    V x x

()    =    ()

(V_1,V_2)    =    V_1x_1 V_2 x_2 (x_1,x_2)

M    =    M

V    =    V x x

The translation is type-preserving and the identity from 's point of view

For any  term $\Gamma \pipe \Delta \vdash E : T$, $\simp E$
is a term of  satisfying $\Gamma, \simp\Delta \vdash \simp E :
\simp T$ where
$\simp{\cdot} = \cdot$ $\simpp{\bullet:\u B} = z:U\u B$,
$\simp{\u B} = \u B$, $\simp A = \u F A$.

Considering CBPV as a subset of   we have

* If $\Gamma \pipe \cdot \vdash M : \u B$  then $M \equidyn \simp M$.

* If $\Gamma \pipe \Delta \vdash S : \u B$ then $S[\force z] \equidyn \simp S$.

* If $\Gamma \vdash V : A$ then $\ret V \equidyn \simp V$.

Furthermore, if $M, V, S$ are in , the proof holds in .

Finally, we need to show that the translation preserves inequalities
($\simp{E} \ltdyn \simp{E'}$ if $E \ltdyn E'$), but because complex
values and stacks satisfy more equations than arbitrary computations in
the types of their translations do, we need to isolate the special
“purity” property that their translations have.

We show that complex values are translated to computations that satisfy
thunkability <cit.>, which

intuitively means $M$ should have no observable effects, and so
can be freely duplicated or discarded like a value.

In the inequational theory of , this is defined by saying that
running $M$ to a value and then duplicating its value is the same as
running $M$ every time we need its value:

A computation $\Gamma \vdash M : \u FA$ is thunkable if

\[\Gamma \vdash \ret{( \thunk M)} \equidyn \bindXtoYinZ M x \ret{(\thunk (\ret x))} : \u FU\u F A\]

Dually, we show that complex stacks are translated to computations that
satisfy (semantic) linearity <cit.>, where intuitively a computation $M$
with a free variable $x : U \u B$ is linear in $x$ if $M$ behaves as if
when it is forced, the first thing it does is forces $x$, and that is the only time
it uses $x$.  This is described in the CBPV inequational theory as
if we have a thunk $z : U\u F U \u B$, then either we can force
it now and pass the result to $M$ as $x$, or we can just run $M$ with a
thunk that will force $z$ each time $M$ is forced—but if $M$ forces
$x$ exactly once, first, these two are the same.

A term $\Gamma, x : U\u B \vdash M : \u C$ is linear in $x$

\[ \Gamma, z : U\u FU\u B \vdash
\bindXtoYinZ {\force z} x M
\equidyn M[\thunk{(\bindXtoYinZ {(\force z)} x \force x)}]
\]

Thunkability/linearity of the translations of complex values/stacks are
used to prove the preservation of the $\eta$ principles for positive
types and the strictness of complex stacks with respect to errors under

Composing this with the translation from GTT to
shows that GTT value upcasts are thunkable and computation
downcasts are linear, which justifies a number of program transformations.

We need a few lemmas about thunkables and linears to prove that complex
values become thunkable and complex stacks become linear.

First, the following lemma is useful for optimizing programs with
thunkable subterms.  Intuitively, since a thunkable has “no effects”
it can be reordered past any other effectful binding.  Furhmann
<cit.> calls a morphism that has this property
central (after the center of a group, which is those elements
that commute with every element of the whole group).

If $\Gamma \vdash M : \u F A$ is thunkable and $\Gamma \vdash N : \u
F A'$ and $\Gamma , x:A, y:A' \vdash N' : \u B$, then

\[
\bindXtoYinZ M x \bindXtoYinZ N y N'
\equidyn
\bindXtoYinZ N y \bindXtoYinZ M x N'
\]

\begin{align*}
&\bindXtoYinZ M x \bindXtoYinZ N y N'\\
\bindXtoYinZ M x \bindXtoYinZ N y \bindXtoYinZ {\force \thunk \ret x} x N' \tag{$U\beta,\u F\beta$}\\
&\equidyn\bindXtoYinZ M x \bindXtoYinZ {\ret\thunk\ret x} w \bindXtoYinZ N y \bindXtoYinZ {\force w} x N' \tag{$\u F\beta$}\\
&\equidyn\bindXtoYinZ {(\bindXtoYinZ M x {\ret\thunk\ret x})} w \bindXtoYinZ N y \bindXtoYinZ {\force w} x N' \tag{$\u F\eta$}\\
&\equidyn\bindXtoYinZ {\ret \thunk M} w \bindXtoYinZ N y \bindXtoYinZ {\force w} x N' \tag{$M$ thunkable}\\
&\equidyn\bindXtoYinZ N y \bindXtoYinZ {\force \thunk M} x N' \tag{$\u F\beta$}\\
&\equidyn\bindXtoYinZ N y \bindXtoYinZ M x N' \tag{$U\beta$}\\
\end{align*}

Next, we show thunkables are closed under composition and that return
of a value is always thunkable.  This allows us to easily build up
bigger thunkables from smaller ones.

If $\Gamma \vdash M : \u F A$ and $\Gamma, x : A \vdash N : \u F A'$
are thunkable, then

\[ \bindXtoYinZ M x N \]

is thunkable.

\begin{align*}
&\bindXtoYinZ {(\bindXtoYinZ M x N)} y \ret\thunk\ret y\\
&\equidyn \bindXtoYinZ M x \bindXtoYinZ N y \ret\thunk\ret y\tag{$\u F\eta$}\\
&\equidyn \bindXtoYinZ M x \ret \thunk N \tag{$N$ thunkable}\\
&\equidyn \bindXtoYinZ M x \ret \thunk (\bindXtoYinZ {\ret x} x N)\tag{$\u F\beta$}\\
&\equidyn \bindXtoYinZ M x \bindXtoYinZ {\ret\thunk\ret x} w \ret \thunk (\bindXtoYinZ {\force w} x N)\tag{$\u F\beta,U\beta$}\\
&\equidyn \bindXtoYinZ {(\bindXtoYinZ M x \ret\thunk\ret x)} w \ret \thunk (\bindXtoYinZ {\force w} x N)\tag{$\u F\eta$}\\
&\equidyn \bindXtoYinZ {\ret\thunk M} w \ret \thunk (\bindXtoYinZ {\force w} x N)\tag{$M$ thunkable}\\
&\equidyn  \ret \thunk (\bindXtoYinZ {\force \thunk M} x N)\tag{$\u F\beta$}\\
&\equidyn  \ret \thunk (\bindXtoYinZ {M} x N)\tag{$U\beta$}\\
\end{align*}

If $\Gamma \vdash V : A$ then $\ret V$ is thunkable.

By $\u F\beta$:

\[ \bindXtoYinZ {\ret V} x \ret\thunk\ret x \equidyn \ret\thunk\ret V \]

If $\Gamma \vdash V : A$ is a (possibly) complex value, then $\Gamma
\vdash \simp V : \u F A$ is thunkable.

Introduction forms follow from return is thunkable and thunkables
compose. For elimination forms it is sufficient to show that when
the branches of pattern matching are thunkable, the pattern match
is thunkable.

* $x$: We need to show $\simp x = \ret x$ is thunkable, which we
proved as a lemma above.

*  $0$ elim, we need to show

\[ \bindXtoYinZ {\absurd V} y \ret\thunk\ret y\equidyn \ret\thunk {\absurd V}\]

but by $\eta0$ both sides are equivalent to $\absurd V$.

*  $+$ elim, we need to show

\[
\ret\thunk (\caseofXthenYelseZ V {x_1. M_1} {x_2. M_2})
\equidyn
\bindXtoYinZ {(\caseofXthenYelseZ V {x_1. M_1} {x_2. M_2})} y \ret\thunk \ret y
\]

\begin{align*}
&\ret\thunk (\caseofXthenYelseZ V {x_1. M_1} {x_2. M_2})\\
\caseofX V \tag{$+\eta$}\\
&\qquad\thenY {x_1. \ret\thunk (\caseofXthenYelseZ {\inl x_1} {x_1. M_1} {x_2. M_2})}\\
&\qquad\elseZ {x_2. \ret\thunk (\caseofXthenYelseZ {\inr x_2} {x_1. M_1} {x_2. M_2})}\\
&\equidyn\caseofX V \tag{$+\beta$}\\
&\qquad\thenY {x_1. \ret\thunk M_1}\\
&\qquad\elseZ {x_2. \ret\thunk M_2}\\
&\equidyn\caseofX V \tag{$M_1,M_2$ thunkable}\\
&\qquad\thenY {x_1. \bindXtoYinZ {M_1} y \ret\thunk\ret y}\\
&\qquad\elseZ {x_2. \bindXtoYinZ {M_2} y \ret\thunk\ret y}\\
&\equidyn \bindXtoYinZ {(\caseofXthenYelseZ V {x_1. M_1}{x_2. M_2})} y \ret\thunk\ret y\tag{commuting conversion}\\
\end{align*}

*  $\times$ elim

\begin{align*}
&\ret\thunk (\pmpairWtoXYinZ V x y M)\\
&\equidyn \pmpairWtoXYinZ V x y \ret\thunk \pmpairWtoXYinZ {(x,y)} x y M\tag{$\times\eta$}\\
&\equidyn \pmpairWtoXYinZ V x y \ret\thunk M\tag{$\times\beta$}\\
&\equidyn \pmpairWtoXYinZ V x y \bindXtoYinZ M z \ret\thunk\ret z\tag{$M$ thunkable}\\
&\equidyn \bindXtoYinZ {(\pmpairWtoXYinZ V x y M)} z \ret\thunk\ret z\tag{commuting conversion}
\end{align*}

* $1$ elim

\begin{align*}
&\ret\thunk (\pmpairWtoinZ V x y M)\\
&\equidyn \pmpairWtoinZ V \ret\thunk \pmpairWtoinZ {()} M\tag{$1\eta$}\\
&\equidyn \pmpairWtoinZ V \ret\thunk M\tag{$1\beta$}\\
&\equidyn \pmpairWtoinZ V \bindXtoYinZ M z \ret\thunk\ret z\tag{$M$ thunkable}\\
&\equidyn \bindXtoYinZ {(\pmpairWtoinZ V M)} z \ret\thunk\ret z\tag{commuting conversion}
\end{align*}

* $\mu$ elim

\begin{align*}
&\ret\thunk (\pmmuXtoYinZ V x M)\\
&\equidyn \pmmuXtoYinZ V x \ret\thunk \pmmuXtoYinZ {\roll x} x M\tag{$\mu\eta$}\\
&\equidyn \pmmuXtoYinZ V x \ret\thunk M\tag{$\mu\beta$}\\
&\equidyn \pmmuXtoYinZ V x \bindXtoYinZ M y \ret\thunk\ret y\tag{$M$ thunkable}\\
&\equidyn \bindXtoYinZ {(\pmmuXtoYinZ V x M)} y \ret\thunk\ret y\tag{commuting conversion}
\end{align*}

Dually, we have that a stack out of a force is linear and that linears
are closed under composition, so we can easily build up bigger linear
morphisms from smaller ones.

If $\Gamma \pipe \bullet : \u B \vdash S : \u C$, then
$\Gamma , x : U\u B\vdash S[\force x] : \u B$ is linear in $x$.

\begin{align*}
S[\force \thunk {(\bindXtoYinZ {\force z} x \force x)}]
S[{(\bindXtoYinZ {\force z} x \force x)}]\tag{$U\beta$}\\
&\equidyn \bindXtoYinZ {\force z} x S[\force x] \tag{$\u F\eta$}
\end{align*}

If $\Gamma , x : U \u B \vdash M : \u B'$ is linear in $x$ and
$\Gamma , y : \u B' \vdash N : \u B''$ is linear in $y$, then
$\Gamma , x : U \u B \vdash N[\thunk M/y] : $

\begin{align*}
&N[\thunk M/y][\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]\\
&= N[\thunk {(M[\thunk{(\bindXtoYinZ {\force z} x \force x)}])}/y]\\
&\equidyn N[\thunk {(\bindXtoYinZ {\force z} x M)}/y]\tag{$M$ linear}\\
&\equidyn N[\thunk{(\bindXtoYinZ {\force z} x \force \thunk M)}/y] \tag{$U\beta$}\\
N[\thunk{(\bindXtoYinZ {\force z} x \bindXtoYinZ {\ret\thunk M} y \force y)}/y] \tag{$\u F\beta$}\\
N[\thunk{(\bindXtoYinZ {(\bindXtoYinZ {\force z} x \ret\thunk M)} y \force y)}/y] \tag{$\u F\eta$}\\
N[\thunk{(\bindXtoYinZ {\force w} y \force y)}/y][\thunk(\bindXtoYinZ {\force z} x \ret\thunk M)/w] \tag{$U\beta$}\\
&\equidyn (\bindXtoYinZ {\force w} y N)[\thunk (\bindXtoYinZ {\force z} x \ret \thunk M)/w] \tag{$N$ linear}\\
&\equidyn (\bindXtoYinZ {(\bindXtoYinZ {\force z} x \ret \thunk M)} y N) \tag{$U\beta$}\\
&\equidyn (\bindXtoYinZ {\force z} x \bindXtoYinZ {\ret\thunk M} y N \tag{$\u F\eta$}\\
&\equidyn \bindXtoYinZ {\force z} x N[\thunk M/y]
\end{align*}

If $\Gamma\pipe \bullet : \u B \vdash S : \u C$ is a (possibly)
complex stack, then $\Gamma, z : U\u B \vdash \simpp{S} : \u C$ is linear in $z$.

There are $4$ classes of rules for complex stacks: those that are
rules for simple stacks ($\bullet$, computation type elimination
forms), introduction rules for negative computation types where the
subterms are complex stacks, elimination of positive value types
where the continuations are complex stacks and finally application
to a complex value.

The rules for simple stacks are easy: they follow immediately from
the fact that forcing to a stack is linear and that complex stacks
compose.  For the negative introduction forms, we have to show that
binding commutes with introduction forms. For pattern matching
forms, we just need commuting conversions. For function application,
we use the lemma that binding a thunkable in a linear term is

* $\bullet$: This is just saying that $\force z$ is linear,
which we showed above.

* $\to$ elim We need to show, assuming that $\Gamma, x : \u B
\vdash M : \u C$ is linear in $x$ and $\Gamma \vdash N : \u F A$
is thunkable, that

\[
\bindXtoYinZ N y M\,y
\]

is linear in $x$.

\begin{align*}
&\bindXtoYinZ N y (M[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x])\,y\\
&\equidyn \bindXtoYinZ N y (\bindXtoYinZ {\force z} x M)\,y \tag{$M$ linear in $x$}\\
&\equidyn \bindXtoYinZ N y \bindXtoYinZ {\force z} x M\,y \tag{$\u F\eta$}\\
&\equidyn \bindXtoYinZ {\force z} x \bindXtoYinZ N y M\,y\tag{thunkables are central}
\end{align*}

* $\to$ intro

\begin{align*}
& \lambda y:A. M[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]\\
&\equidyn \lambda y:A. \bindXtoYinZ {\force z} x M \tag{$M$ is linear}\\
&\equidyn \lambda y:A. \bindXtoYinZ {\force z} x (\lambda y:A. M)\, y \tag{$\to\beta$}\\
&\equidyn \lambda y:A. (\bindXtoYinZ {\force z} x (\lambda y:A. M))\, y \tag{$\u F\eta$}\\
&\equidyn \bindXtoYinZ {\force z} x (\lambda y:A. M) \tag{$\to\eta$}
\end{align*}

* $\top$ intro
We need to show

\[ \bindXtoYinZ {\force z} w \{\} \equidyn \{\} \]

Which is immediate by $\top\eta$

* $\with$ intro

\begin{align*}
&     \pairone{M[\thunk {(\bindXtoYinZ {\force z} x \force x)}]/x}\\
&\pairtwo{N[\thunk {(\bindXtoYinZ {\force z} x \force x)}/x]}\\
&\equidyn \pairone{\bindXtoYinZ {\force z} x M}\tag{$M, N$ linear}\\
&\qquad    \pairtwo{\bindXtoYinZ {\force z} x N}\\
&\equidyn \pairone{\bindXtoYinZ {\force z} x {\pi \pair M N}}\tag{$\with\beta$}\\
&\qquad    \pairtwo{\bindXtoYinZ {\force z} x {\pi' \pair M N}}\\
&\equidyn \pairone{\pi({\bindXtoYinZ {\force z} x \pair M N})}\tag{$\u F\eta$}\\
&\qquad    \pairtwo{\pi'({\bindXtoYinZ {\force z} x \pair M N})}\\
&\equidyn \bindXtoYinZ {\force z} x \pair M N\tag{$\with\eta$}
\end{align*}

* $\nu$ intro

\begin{align*}
& \roll M[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]\\
&\equidyn \roll (\bindXtoYinZ {\force z} x M) \tag{$M$ is linear} \\
&\equidyn \roll (\bindXtoYinZ {\force z} x \unroll \roll M) \tag{$\nu\beta$}\\
&\equidyn \roll \unroll (\bindXtoYinZ {\force z} x \roll M) \tag{$\u F\eta$}\\
&\equidyn \bindXtoYinZ {\force z} x (\roll M) \tag{$\nu\eta$}
\end{align*}

* $\u F$ elim: Assume $\Gamma, x : A \vdash M : \u F A'$ and
$\Gamma, y : A' \vdash N : \u B$, then we need to show

\[ \bindXtoYinZ M y N \]

is linear in $M$.

\begin{align*}
& \bindXtoYinZ {M[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]} y N\\
& \equidyn
\bindXtoYinZ {(\bindXtoYinZ {\force z} x M)} y N\tag{$M$ is linear}\\
\bindXtoYinZ {\force z} x \bindXtoYinZ M y N\tag{$\u F\eta$}
\end{align*}

* $0$ elim: We want to show $\Gamma, x:U\u B \vdash \absurd V :
\u C$ is linear in $x$, which means showing:

\[ \absurd V \equidyn \bindXtoYinZ {\force z} x \absurd V
\]

which follows from $0\eta$

* $+$ elim: Assuming $\Gamma, x : U\u B, y_1 : A_1 \vdash M_1 :
\u C$ and $\Gamma, x : U\u B, y_2: A_2\vdash M_2 : \u C$ are
linear in $x$, and $\Gamma \vdash V : A_1 + A_2$, we need to show

\[ \caseofXthenYelseZ V {y_1. M_1} {y_2. M_2} \]

is linear in $x$.

\begin{align*}
& \caseofX V\\
& \,\,\thenY {y_1. M_1[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]}\\
& \,\,\elseZ {y_2. M_2[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]}\\
&\equidyn \caseofXthenYelseZ V {y_1. \bindXtoYinZ {\force z} x M_1}{y_2. \bindXtoYinZ {\force z} x M_2}\tag{$M_1,M_2$ linear}\\
\bindXtoYinZ {\force z} x \caseofXthenYelseZ V {y_1. M_1}{y_2. M_2}
\end{align*}

* $\times$ elim: Assuming $\Gamma, x:U\u B, y_1 : A_1, y_2 : A_2
\vdash M : \u B$ is linear in $x$ and $\Gamma \vdash V : A_1
\times A_2$, we need to show

\[ \pmpairWtoXYinZ V {y_1}{y_2} M \]

is linear in $x$.

\begin{align*}
&\pmpairWtoXYinZ V {y_1}{y_2} M[[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]]\\
&\equidyn \pmpairWtoXYinZ V {y_1}{y_2} \bindXtoYinZ {\force z} x M\tag{$M$ linear}\\
&\equidyn  \bindXtoYinZ {\force z} x\pmpairWtoXYinZ V {y_1}{y_2} M\tag{comm. conv}\\
\end{align*}

* $\mu$ elim: Assuming $\Gamma , x : U \u B, y : A[\mu X.A/X]
\vdash M : \u C$ is linear in $x$ and $\Gamma \vdash V : \mu X.A$,
we need to show

\[ \pmmuXtoYinZ V y M \]

is linear in $x$.

\begin{align*}
& \pmmuXtoYinZ V y M[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]\\
& \equidyn \pmmuXtoYinZ V y \bindXtoYinZ {\force z} x M\tag{$M$ linear}\\
&\equidyn  \bindXtoYinZ {\force z} x\pmmuXtoYinZ V y M \tag{commuting conversion}
\end{align*}

Composing this with the previous translation from GTT to
shows that GTT value type upcasts are thunkable and computation
type downcasts are linear.

Since the translation takes values and stacks to terms, it cannot
preserve substitution up to equality.

Rather, we get the following, weaker notion that says that the
translation of a syntactic substitution is equivalent to an effectful

* If $\Gamma, x : A\pipe \Delta\vdash E : T$ and $\Gamma \vdash V : A$
are complex terms, then

\[
\simpp{E[V/x]} \equidyn \bindXtoYinZ {\simp V} x {\simp E}
\]

* If $\Gamma \pipe \bullet : \u B \vdash S : \u C$ and $\Gamma
\pipe \Delta \vdash M : \u B$, then

\[
\simpp{S[M]} \equidyn \simp{S}[\thunk\simp{M}/z]
\]

* First, note that every occurrence of a variable in $\simp E$ is of
the form $\ret x$ for some variable $x$. This means we can define
substitution of a term for a variable in a simplified term by
defining $\simp{E}[N/\ret x]$ to replace every $\ret x : \u F A$
with $N : \u F A$. Then it is an easy observation that
simplification is compositional on the nose with respect to this
notion of substitution:

\[ \simpp{E[V/x]} = \simp{E}[\simp V / \ret x] \]

Next by repeated invocation of $U\beta$,

\[ \simp{E}[\simp V/\ret x] \equidyn \simp{E}[\force\thunk\simp V/\ret x] \]

Then we can lift the definition of the thunk to the top-level by $\u F\beta$:

\[ \simp{E}[\force\thunk\simp V/\ret x] \equidyn
\bindXtoYinZ \ret\thunk \simp V w \simp{E}[\force w/\ret x]
\]

Then because $\simp V$ is thunkable, we can bind it at the top-level
and reduce an administrative redex away to get our desired result:

\begin{align*}
&\bindXtoYinZ \ret\thunk \simp V w \simp{E}[\force w/\ret x]\\
&\equidyn \bindXtoYinZ {\simp V} x \bindXtoYinZ {\ret\thunk\ret x} w \simp{E}[\force w/\ret x]\tag{$V$ thunkable}\\
&\equidyn \bindXtoYinZ {\simp V} x \simp{E}[\force \thunk\ret x/\ret x]\tag{$\u F\beta$}\\
&\equidyn \bindXtoYinZ {\simp V} x \simp{E}[\ret x/\ret x]\tag{$U\beta$}\\
&\equidyn \bindXtoYinZ {\simp V} x \simp{E}\\
\end{align*}

* Note that every occurrence of $z$ in $\simp S$ is of the form
$\force z$. This means we can define substitution of a term
$M : \u B$ for $\force z$ in $\simp S$ by replacing $\force z$
with $M$.  It is an easy observation that simplification is
compositional on the nose with respect to this notion of

\[ \simpp{S[M/\bullet]} = \simp S[\simp M/\force z] \]

Then by repeated $U\beta$, we can replace $\simp M$ with a forced thunk:

\[ \simp S[\simp M/\force z] \equidyn \simp S[\force\thunk \simp M/\force z] \]

which since we are now substituting a force for a force is the
same as substituting the thunk for the variable:

\[ \simp S[\force\thunk \simp M/\force z]
\equidyn
\simp S[\thunk \simp M / z]
\]

If $\Gamma \pipe \Delta \vdash E \ltdyn E' : T$ then ${\Gamma, \simp
\Delta \vdash \simp E \ltdyn \simp{E'} : \simp T}$

* Reflexivity is translated to reflexivity.

* Transitivity is translated to transitivity.

* Compatibility rules are translated to compatibility rules.

* Substitution of a Value

\[
\inferrule
{\Gamma, x : A, \simp\Delta \vdash \simp E \ltdyn \simp {E'} : \simp T \and \Gamma \vdash \simp V \ltdyn \simp {V'} : \u F A}
{\Gamma, \simp\Delta \vdash \simp{E[V/x]} \ltdyn \simp{E'[V'/x]} : \simp T}
\]

By the compositionality lemma, it is sufficient to show:

\[ \bindXtoYinZ {\simp V} x {\simp E} \ltdyn \bindXtoYinZ {\simp {V'}} {x} E' \]

which follows by bind compatibility.

* Plugging a term into a hole:

\[
\inferrule
{\Gamma, z : U{\u C} \vdash \simp {S} \ltdyn \simp{S'} : \u B\and
\Gamma,\simp\Delta \vdash \simp{M} \ltdyn \simp{M'} : \u C}
{\Gamma, \simp\Delta \vdash \simp{S[M]} \ltdyn \simp{S'[M']} : \u B}
\]

By compositionality, it is sufficient to show

\[ \simp{S}[\thunk{\simp M}/z] \ltdyn \simp{S'}[\thunk{\simp{M'}}/z] \]

which follows by thunk compatibility and the simple substitution rule.

* Stack strictness
We need to show for $S$ a complex stack,

\[ \simpp{S[\err]} \equidyn \err \]

By stack compositionality we know

\[ \simpp{S[\err]} \equidyn \simp{S}[{\thunk \err/z}] \]

\begin{align*}
\sem{S}[{\thunk \err/z}]
&\equidyn \simp{S}[\thunk {(\bindXtoYinZ \err y \err)}/z]\tag{Stacks preserve $\err$}\\
\bindXtoYinZ \err y \simp{S}[{\thunk \err/z}] \tag{$\simp S$ is linear in $z$}\\
&\equidyn \err \tag{Stacks preserve $\err$}
\end{align*}

* $1\beta$ By compositionality it is sufficient to show

\[\bindXtoYinZ {\ret ()} x \pmpairWtoinZ x {\simp E} \equidyn \bindXtoYinZ {\ret ()} x \simp E \]

which follows by $\u F\beta, 1\beta$.

* $1\eta$ We need to show for $\Gamma, x : 1 \pipe \Delta \vdash E : T$

\[ \simp{E} \equidyn \bindXtoYinZ {\ret x} x \pmpairWtoinZ x {\simpp{E[()/x]}}\]

after a $\u F\beta$, it is sufficient using $1\eta$ to prove:

\[ {\simpp{E[()/x]}} \equidyn \simp E[()/x] \]

which follows by compositionality and $\u F\beta$:

\[ {\simpp{E[()/x]}} \equidyn \bindXtoYinZ {\ret ()} x {\simp E} \equidyn \simp{E}[()/x] \]

* $\times\beta$ By compositionality it is sufficient to show

\begin{align*}
&\bindXtoYinZ {(\bindXtoYinZ {\simp{V_1}} {x_1} \bindXtoYinZ {\simp{V_2}} {x_2} {\ret (x_1,x_2)})} x \pmpairWtoXYinZ {x} {x_1}{x_2} {\simp E}\\
&\equidyn \bindXtoYinZ {\simp{V_1}} {x_1} \bindXtoYinZ {\simp{V_2}} {x_2} \simp E
\end{align*}

which follows by $\u F\eta, \u F\beta, \times\beta$.

* $\times\eta$ We need to show for $\Gamma, x : A_1\times A_2
\pipe\Delta \vdash E : T$ that

\[ \simp{E} \equidyn \bindXtoYinZ {\ret x} x \pmpairWtoXYinZ x {x_1}{x_2} \simpp{E[(x_1,x_2)/x]} \]

by $\u F\beta,\times\eta$ it is sufficient to show

\[ \simp{E[(x_1,x_2)/x]} \equidyn \simp{E}[(x_1,x_2)/x] \]

Which follows by compositionality:

\begin{align*}
&\equidyn \bindXtoYinZ {x_1}{x_1}\bindXtoYinZ {x_2}{x_2} \bindXtoYinZ {\ret (x_1,x_2)} x \simp E\tag{compositionality}\\
&\equidyn \bindXtoYinZ {\ret (x_1,x_2)} x \simp E\tag{$\u F\beta$}\\
&\equidyn \simp E[(x_1,x_2)/x]
\end{align*}

* $0\eta$
We need to show for any $\Gamma, x : 0 \pipe \Delta \vdash E : T$

\[ \simp E \equidyn \bindXtoYinZ {\ret x} x \absurd x \]

which follows by $0\eta$

* $+\beta$ Without loss of generality, we do the $\inl$ case
By compositionality it is sufficient to show

\[
\bindXtoYinZ {(\bindXtoYinZ {\simp V} x {\inl x})} x \caseofXthenYelseZ x {x_1. \simp E_1}{x_2. \simp E_2}
\equidyn \simp{E_1[V/x_1]}
\]

which holds by $\u F\eta,\u F\beta, +\beta$

* $+\eta$ We need to show for any $\Gamma, x:A_1+A_2
\pipe\Delta\vdash E :T$ that

\[ \simp E \equidyn
\bindXtoYinZ {\ret x} x \caseofXthenYelseZ x {x_1. \simpp{E[\inl x_1/x]}}{x_2. \simpp{E[\inl x_2/x]}} \]

\begin{align*}
&\simp E\\
&\equidyn \caseofXthenYelseZ x {x_1. \simp{E}[\inl x_1/x]}{x_2. \simp{E}[\inl x_2/x]} \tag{$+\eta$}\\
\caseofXthenYelseZ x {x_1. \bindXtoYinZ {\ret \inl x_1} x \simp{E}}{x_2. \bindXtoYinZ {\ret \inl x_2} x \simp{E}}\tag{$\u F\beta$}\\
\caseofXthenYelseZ x {x_1. \simp{E[\inl x_1]/x}}{x_2. \simp{E[\inl x_2]/x}}\tag{compositionality}\\
\bindXtoYinZ {\ret x} x \caseofXthenYelseZ x {x_1. \simp{E[\inl x_1]/x}}{x_2. \simp{E[\inl x_2]/x}}\tag{$\u F\beta$}
\end{align*}

* $\mu\beta$ By compositionality it is sufficient to show

\begin{align*}
&\bindXtoYinZ {(\bindXtoYinZ {\simp V} y {\ret \roll y})} x \pmmuXtoYinZ {x} y E\\
&\equidyn \bindXtoYinZ {\simp V} y \simp E
\end{align*}

which follows by $\u F\eta, \u F\beta, \mu\beta$.

* $\mu\eta$ We need to show for $\Gamma, x : \mu X. A \pipe\Delta \vdash E : T$ that

\[ \simp{E} \equidyn \bindXtoYinZ {\ret x} x \pmmuXtoYinZ x y \simpp{E[\roll y/x]} \]

by $\u F\beta,\times\eta$ it is sufficient to show

\[ \simp{E[\roll y/x]} \equidyn \simp{E}[\roll y/x] \]

Which follows by compositionality:

\begin{align*}
&\simp{E[\roll y/x]}\\
&\equidyn \bindXtoYinZ {\ret y} y \bindXtoYinZ {\ret \roll y} x \simp E\tag{compositionality}\\
&\equidyn \bindXtoYinZ {{\ret\roll y}} x \simp E\tag{$\u F\beta$}\\
&\equidyn \simp E[\roll y/x] \tag{$\u F\beta$}
\end{align*}

* $U\beta$ We need to show

\[ \bindXtoYinZ {\ret \simp M} x {\force x} \equidyn \simp M \]

which follows by $\u F\beta, U\beta$

* $U\eta$ We need to show for any $\Gamma \vdash V : U\u B$ that

\[ \simp V \equidyn \ret \thunk{(\bindXtoYinZ {\simp V} x \force x)}\]

By compositionality it is sufficient to show

\[ \simp V \equidyn \bindXtoYinZ {\simp V} x \ret\thunk{(\bindXtoYinZ {\ret x} x \force x)}\]

which follows by $U\eta$ and some simple reductions:

\begin{align*}
\bindXtoYinZ {\simp V} x \ret\thunk{(\bindXtoYinZ {\ret x} x \force x)}\\
&\equidyn \bindXtoYinZ {\simp V} x\ret\thunk{\force x}\tag{$\u F\beta$}\\
&\equidyn \bindXtoYinZ {\simp V} x\ret x\tag{$U\eta$}\\
&\equidyn \simp V\tag{$\u F\eta$}
\end{align*}

* $\to\beta$
By compositionality it is sufficient to show

\[ \bindXtoYinZ {\simp V} x (\lambda x:A. \simp M)\,x
\equidyn \bindXtoYinZ {\simp V} x \simp M \]

which follows by $\to\beta$

* $\to\eta$ We need to show

\[ z : U(A \to \u B) \vdash
\force z \equidyn
\lambda x:A. \bindXtoYinZ {\ret x} x (\force z)\,x
\]

which follows by $\u F\beta, \to\eta$

* $\top\eta$ We need to show

\[ z : U\top \vdash \force z \equidyn \{\} \]

which is exactly $\top\eta$.

* $\with\beta$ Immediate by simple $\with\beta$.

* $\with\eta$ We need to show