more response edits (900 still)

popl19/response2.md

 We thank the reviewers for their very helpful feedback and will revise
 the paper accordingly. In particular, we will expand on the motivation
-for using CBPV.
+for using CBPV and clearly state our contributions.
 
 1. Reviewer C says "Moreover, the paper doesn't produce any particular
    equalities that one might want to reason with while programming."
@@ -29,7 +29,7 @@ contextually equivalent. We do include beta-eta in the definition of
 term dynamism in figure 4, where they are labeled as axioms of term
 dynamism, but this is not enough to prove completeness for an
 effectful language like cbpv: for instance, both sequential and
-non-deterministic languages should model all of the axioms.
+non-deterministic languages model beta-eta.
 
 The syntax is not intended to be complete for any particular language,
 in order that it apply to as many as possible. This is what allows us
@@ -57,7 +57,7 @@ https://newtraell.cs.uchicago.edu/research/publications/techreports/TR-2004-02
 4. Reviewer D asks to clarify lines 116-117.
 
 Yes, we mean that the typed equivalences should hold in the statically
-typed portions of the code; the dynamic type casts ensure that the
+typed portions of the code; but the casts ensure that the
 equivalences hold in statically typed portions of the code even if they
 interact with (more) dynamically typed code. We expect that it will be
 rare for gradually typed programs to be completely typed (e.g. this is
@@ -85,7 +85,7 @@ effects.
 7. Reviewer A asks "(l35) eta is mostly used in one direction for optimization, it's
     the other direction that fails for these cases right?"
 
-Yes, in the "eager" cast semantics, the eta law for functions should be
+Yes, in the eager cast semantics, the eta law for functions should be
 an ordering `V <= \x -> V x` but it's debateable whether this means that
 the right should be allowed to be optimized to the left. This would make
 the semantics of the program dependent on the precise behavior of the