corrections.org 1.39 KiB
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.