TODO.org

* 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