From 34224a0cc42bd9af83b0b3aaf1402d560eba4202 Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Mon, 9 Jul 2018 15:03:59 -0400
Subject: [PATCH] abstract

---
 paper/abstract.tex | 66 ++++++++++++++++++++++------------------------
 paper/gtt.tex      |  4 +--
 2 files changed, 34 insertions(+), 36 deletions(-)

diff --git a/paper/abstract.tex b/paper/abstract.tex
index 6b549cc..7d09bcf 100644
--- a/paper/abstract.tex
+++ b/paper/abstract.tex
@@ -1,34 +1,32 @@
-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 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.   
-
-In this paper, we propose an \emph{axiomatic} account of program equivalence in a
-gradual cast calculus, which we formalize in a logic we call \emph{gradual type
-theory} (GTT). Based on Levy's call-by-push-value, GTT gives an axiomatic account
-of both call-by-value and call-by-name gradual languages.
-
-Based on our axiomatic account we prove many theorems that justify optimizations
-and refactorings in gradually typed languages. For example, we show what we call
-\emph{uniqueness principles} for gradual type connectives that show that if the
-$\beta\eta$ laws hold for a connective, then casts between that connective must
-be equivalent to the ``lazy'' cast semantics. 
-As a contrapositive, this shows that ``eager'' cast semantics violates the
-extensionality of function types.  Additionally, we show that gradual upcasts
-are pure functions and, dually, gradual downcasts are strict functions, an
-equational analogue of Wadler-Findler's blame soundness theorem.
-
-We show the consistency and applicability of our axiomatic theory by proving
-that a contract-based implementation using the lazy cast semantics gives a model
-of our type theory where equivalence in GTT implies contextual equivalence of
-the programs.  Since GTT also axiomatizes the dynamic gradual guarantee, our
-logical relation also establishes this central theorem of gradual typing.
-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
+Gradually typed languages are designed to support both dynamically typed
+and statically typed programming styles while preserving the benefits of
+each.  While existing 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 correctness of type-based refactorings and optimizations
+is preserved.  Establishing correctness of program transformations is
+technically difficult, because it requires reasoning about program
+equivalence, and is often neglected in the metatheory of gradual
+languages.  In this paper, we propose an \emph{axiomatic} account of
+program equivalence in a gradual cast calculus, which we formalize in a
+logic we call \emph{gradual type theory} (GTT). Based on Levy's
+call-by-push-value, GTT gives an axiomatic account of both call-by-value
+and call-by-name gradual languages.  Based on our axiomatic account we
+prove many theorems that justify optimizations and refactorings in
+gradually typed languages. For example, 
+\emph{uniqueness principles} for gradual type connectives show that if the
+$\beta\eta$ laws hold for a connective, then casts between that
+connective must be equivalent to the so-called ``lazy'' cast semantics.
+Contrapositively, this shows that ``eager'' cast semantics violates the
+extensionality of function types.  As another example, we show that
+gradual upcasts are pure functions and, dually, gradual downcasts are
+strict functions, an equational analogue of Wadler-Findler's blame
+soundness theorem.  We show the consistency and applicability of our
+axiomatic theory by proving that a contract-based implementation using
+the lazy cast semantics gives a logical relations model of our type
+theory, where equivalence in GTT implies contextual equivalence of the
+programs.  Since GTT also axiomatizes the dynamic gradual guarantee, our
+model also establishes this central theorem of gradual typing.  The
+model is parametrized by the implementation of the dynamic types, and so
+gives a family of implementations that validate type-based optimization
+and the gradual guarantee.
diff --git a/paper/gtt.tex b/paper/gtt.tex
index a085ae6..0e8e4a0 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -12,8 +12,8 @@
 \newif\ifshort
 \newif\iflong
 %% Pick long or short version:
-%% \shorttrue
-\longtrue
+\shorttrue
+%% \longtrue
 
 %% Note: Authors migrating a paper from PACMPL format to traditional
 %% SIGPLAN proceedings format should change 'acmlarge' to
-- 
GitLab