From bcd110093651f857264ee75cf43dd19d362f983a Mon Sep 17 00:00:00 2001
From: Amal Ahmed <amal@ccs.neu.edu>
Date: Mon, 29 Oct 2018 17:54:24 -0400
Subject: [PATCH] minor edits
---
paper/gtt.tex | 9 ++++-----
1 file changed, 4 insertions(+), 5 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 1d381bb..f25773d 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -812,7 +812,6 @@ Our modular proof architecture allows us to easily prove correctness
of $\beta, \eta$ and graduality for all of these interpretations.
\textbf{Contributions}
-
The main contributions of the paper are as follows.
\begin{enumerate}
\item We present Gradual Type Theory in section \ref{sec:gtt}, a simple
@@ -9430,13 +9429,13 @@ restriction for call-by-value function $\eta$.
%
We are not aware of any call-by-name gradual languages, but there is
considerable work on \emph{contracts} for non-eager languages,
-especially Haskell, \cite{hinzeJeuringLoh06,XuPJC09}.
+especially Haskell \cite{hinzeJeuringLoh06,XuPJC09}.
%
However, we note that Haskell is \emph{not} a call-by-name language in
our sense for two reasons.
%
First, Haskell uses call-by-need evaluation where results of
-computations are memoized. However when only considering Haskell's
+computations are memoized. However, when only considering Haskell's
effects (error and divergence), this difference is not observable so
this is not the main obstacle.
%
@@ -9473,7 +9472,7 @@ Our work here is complementary, showing that certain program
equivalences can only be achieved by certain cast semantics.
\citet{Degen2012TheIO} give an analysis of different cast semantics
-for contracts in lazy languages, specifically based on Haskell, so
+for contracts in lazy languages, specifically based on Haskell, i.e.,
call-by-need with \seq.
%
They propose two properties ``meaning preservation'' and
@@ -9493,7 +9492,7 @@ non-contracted term.
Completeness, on the other hand, requires that when a contract is
attached to a value that it is \emph{deeply} checked.
%
-The two properties are incompatible because for instance a pair of a
+The two properties are incompatible because, for instance, a pair of a
diverging term and a value can't be deeply checked without causing the
entire program to diverge.
%
--
GitLab