more edits, made reviewers bold

popl19/response2.md

@@ -2,14 +2,13 @@ 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 and clearly state our contributions.
 
-1. Reviewer C says "Moreover, the paper doesn't produce any particular
+1. **Reviewer C** says "Moreover, the paper doesn't produce any particular
    equalities that one might want to reason with while programming."
 
-We disagree: we show soundness of an entire
-class of equalities that are useful for program reasoning by programmers
-and compilers alike: things like lifting an if statement (or more
-generally any pattern match) out of a lambda are very common in
-refactoring and optimization.
+We disagree: we show soundness of an entire class of equalities that are useful
+for program reasoning by programmers and compilers alike: things like lifting an
+if statement (or more generally any pattern match) out of a lambda are very
+common in refactoring and optimization.
 
 In terms of "actionable" theorems, we show that upcasts form complex
 values and downcasts form complex stacks, which also justifies 
@@ -19,8 +18,8 @@ out of loops as if they were values.  Downcasts, as complex stacks, are
 strict in their input, which aids strictness analysis, as in optimizers
 for lazy langauges.
 
-2. Reviewer C asks about the meaning of L514 and whether or not our
-   syntactic theory of term dynamism and equivalence is not only sound
+2. **Reviewer C** asks (Question1) about the meaning of L514 and whether or not
+   our syntactic theory of term dynamism and equivalence is not only sound
    but *complete* for contextual equivalence.
 
 Our sentence is a bit awkwardly worded, but we mean that if two terms
@@ -37,7 +36,7 @@ to interpret the model with incompatible definitions of the dynamic
 type and extend it with new axioms based on that model like those
 given in figure 5.
 
-3. Reviewer C asks "Do these theorems hold when you distinguish
+3. **Reviewer C** asks (Question2) "Do these theorems hold when you distinguish 
    between different errors via, e.g., blame labels?"
 
 It seems likely, but it's not yet clear how to formalize these properties
@@ -54,7 +53,7 @@ when all of the casts involved have the *same* label; we may explore
 this in future work, building on the unpublished tech report:
 https://newtraell.cs.uchicago.edu/research/publications/techreports/TR-2004-02
 
-4. Reviewer D asks to clarify lines 116-117.
+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; but the casts ensure that the
@@ -63,7 +62,7 @@ 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
 very rare in Typed Racket).
 
-5. Reviewer D asks about languages where dynamism doesn't go all the
+5. **Reviewer D** asks about languages where dynamism doesn't go all the
    way up to ? if we can still reduce everything to upcasts and
    downcasts.
 
@@ -72,7 +71,7 @@ with any type D that is more dynamic than both A and B. We don't know
 of any systems where a cast A => B is allowed but they have no common
 dynamism-supertype.
 
-6. Reviewer C says that we "restrict to non-effectful programs" and
+6. **Reviewer C** says that we "restrict to non-effectful programs" and
    finds it surprising because "blame is an effect".
 
 We _do_ treat dynamic type errors as an effect, and as Reviewer D notes, this is
@@ -83,8 +82,8 @@ the eta rule (explaining the eta rule in traditional call-by-value is restricted
 to values or non-effectful code). 
 
 
-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?"
+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
 an ordering `V <= \x -> V x` but it's debateable whether this means that
@@ -95,7 +94,7 @@ either making code error that didn't before or vice-versa (because
 whether or not an optimization is triggered can be very sensitive to
 small changes).
 
-8. Reviewer C comments on some missing related work.
+8. **Reviewer C** comments on some missing related work.
 
 We apologize for the oversight and will add appropriate discussion; for
 Henglein, a significant difference is that the equational theory there