corrections.org

* Typos
  - [X] 111: missing a turnstile, would be better to have on its own line.
  - [X] 687: one of these should be an upcast
  - [X] l475: "that it is true" that what is true?
  - [X] l559: the rule err <= M uses M below and M' above.
  - [X] l898: G should be floor A
* Clarity
  - multiple reviewers: there isn't a "we did this" part of the intro
  - numeric citations as nouns: L1025 and "elsewhere".
  - 108: *dynamic* gradual guarantee
  - "AGT is based on operational semantics more than it's based on
    axiomatic semantics, but it's primarily based on typing—*static*
    semantics.  I got the point eventually, but it was a little
    jarring."
  - CBPV mnemonic: liFt, thUnk
  - You correctly saw the need for a section to give background on
    CBPV, but it's also important to clearly summarize the two papers
    you're generalizing.
* Proper Attribution
  - Blame soundness as a concept is not due to Wadler and Findler, but
    to [Tobin-Hochstadt and Felleisen 2006] , although you may be
    thinking of a more specific result here from Wadler and
    Findler. The argument in this paragraph (the continuation cannot
    affect the result and thus does not deserve blame) is very similar
    to the criteria given in "blame correctness" by [Dimoulas et al
    2011].
  - Our work on constructing models of the dynamic type should cite
    some of the obvious stuff on type tags, type Dynamic, etc.