Gradually typed languages are designed to support both dynamically typed and
statically typed programming styles while preserving the benefits of each.
Gradual type soundness theorems for these languages are aimed at showing that 
type-based reasoning is preserved when moving from the fully static setting to a
gradual one. But gradual type soundness does not imply that type-based
refactorings and optimizations are still sound in the gradual language.  
Unfortunately, establishing the correctness of program transformations is 
technically difficult and often neglected in the metatheory of these languages. 

In this paper, we propose an \emph{axiomatic} account of program equivalence in a
gradual cast calculus, which we formalize in a logic we call \emph{gradual type
theory} (GTT). Based on Levy's call-by-push-value, GTT gives an axiomatic account
of both call-by-value and call-by-name gradual languages.

Based on our axiomatic account we prove many theorems that justify optimizations
and refactorings in gradually typed languages. For example, we show what we call
\emph{uniqueness principles} for gradual type connectives that show that if the
$\beta\eta$ laws hold for a connective, then casts between that connective must
be equivalent to the ``lazy'' cast semantics. 
As a contrapositive, this shows that ``eager'' cast semantics violates the
extensionality of function types.  Additionally, we show that gradual upcasts
are pure functions and dually gradual downcasts are strict functions, an
equational analogue of Wadler-Findler's blame soundness theorem.

We show the consistency and applicability of our axiomatic theory by proving
that a contract-based implementation using the lazy cast semantics gives a model
of our type theory where equivalence in GTT implies contextual equivalence of
the programs.  Since GTT also axiomatizes the dynamic gradual guarantee, our
logical relation also establishes this central theorem of gradual typing.
Finally, we define \emph{multiple} contract-based implementations by varying the
structure of the dynamic types, giving a family of implementations that validate
type-based optimization and the gradual guarantee.

% AA: above "logical relation" comes out of the blue