  Gradually typed languages allow statically typed and dynamically typed code
to interact while maintaining benefits of both styles. The key to reasoning
about these mixed programs is Siek-Vitousek-Cimini-Boyland's (dynamic) gradual
guarantee, which says that giving components of a program more precise types
only adds runtime type checking, and does not otherwise change behavior. In
this paper, we give a semantic reformulation of the gradual guarantee called
graduality. We change the name to promote the analogy that graduality is to
gradual typing what parametricity is to polymorphism. Each gives a
local-to-global, syntactic-to-semantic reasoning principle that is formulated
in terms of a kind of observational approximation.
  Utilizing the analogy, we develop a novel logical relation for proving
graduality. We show that embedding-projection pairs (ep pairs) are to
graduality what relations are to parametricity. We argue that casts between two
types where one is "more dynamic" (less precise) than the other necessarily
form an ep pair, and we use this to cleanly prove the graduality cases for
casts from the ep-pair property. To construct ep pairs, we give an analysis of
the type dynamism relation (also known as type precision or naive subtyping)
that interprets the rules for type dynamism as compositional constructions on
ep pairs, analogous to the coercion interpretation of subtyping.
