Reading list for getting started on Gradual Typing

Which papers would I recommend for getting started on understanding the research on gradual typing? That's a hard question because there are a lot of papers to choose from and, as research papers, their primary goal was not to give a good introduction, but instead to describe some scientific contribution. I really ought to write a proper introduction, but in the mean time, here's my choice of a few papers to get started.

1. Refined Criteria for Gradual Typing
   This paper does a decent job of surveying research related to gradual typing and situating it with respect to other areas of research in programming languages and type systems. The paper includes a modern and, what I would deem canonical, specification of the Gradually Typed Lambda Calculus (GTLC). Finally, the paper gives formal criteria for what it means for a language to be gradually typed, including the gradual guarantee.
2. Blame and Coercion: Together Again for the First Time (alternative location)
   The runtime semantics of a gradually typed language is typically given in two parts: 1) a translation to a cast calculus and 2) an operational semantics for the cast calculus. Nowadays,  I recommend using coercions to express casts because they help to constrain the design space in a good way, they are easily extended to handle blame tracking, and they can be compressed to ensure space efficiency (time too!). This paper defines an easy-to-understand coercion calculus \(\lambda C\) and a space-efficient calculus \(\lambda S\), proves that they are equivalent to the standard cast calculus \(\lambda B\), and also reviews the blame safety theorem.
3. Abstracting Gradual Typing (alternative location)
   This paper presents a general framework based on abstract interpretation for understanding gradual typing and for extending gradual typing to handle languages that make use of other predicates on types, such as subtyping. The framework provides guidance for how to define the consistency relation and for how to derive an operational semantics.

After reading the above papers, there's plenty more to enjoy! See the bibliography maintained by Sam Tobin-Hochstadt.