* TODO Requested Revisions 1) [X] Add names to the rules 1) [X] names everywhere 2) [X] make it not ugly 2) [-] Revise Intro 1) [X] List of Contributions 2) [X] Better overview of eta and the counter examples. 3) [ ] Have co-authors review 3) [-] Related Work 1) [ ] Degen-Thiemann 2) [X] Henglein 3) [ ] AGT * TODO Clarity - 4.1 call-by-push-value is dense - 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. * TODO 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. * TODO Response Issues 1) L514 is unclear, and talk about completeness a little. 2) multiple blame labels 3) Lines 116-117, typed equivalences in static portions of code 4) Gradual Languages where ? doesn't exist: this is actually a strength of this paper 5) restrict to non-effectful programs: 6) "particular equalities one might want to reason with while programming" 7) Eta is only used in one direction