switched to short version; minor edits

paper/abstract.tex

@@ -2,7 +2,7 @@ Gradually typed languages are designed to support both dynamically typed and
 statically typed programming styles while preserving the benefits of each.
 While gradual type soundness theorems for these languages aim to show that 
 ``type-based reasoning'' is preserved when moving from the fully static setting to a
-gradual one, these theorems do not imply that the correctness of type-based
+gradual one, these theorems do not imply that correctness of type-based
 refactorings and optimizations is preserved.  Establishing correctness of
 program transformations is technically difficult---requires reasoning about
 program equivalence---and often neglected in the metatheory of gradual languages.   
@@ -31,4 +31,3 @@ Finally, we define \emph{multiple} contract-based implementations by varying the
 structure of the dynamic types, giving a family of implementations that validate
 type-based optimization and the gradual guarantee.
 
-% AA: above "logical relation" comes out of the blue
\ No newline at end of file