From 07dde6f1feb4429cf87375433173bd74b759e4f6 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Wed, 11 Jul 2018 17:37:42 +0100
Subject: [PATCH] herman cite, monotonic vs proxied in discussion, blame
discussion
---
paper/gtt.tex | 15 +++++++++++++--
paper/max.bib | 9 ++++++++-
2 files changed, 21 insertions(+), 3 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index a3d57c7..87f0551 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -410,7 +410,7 @@ firm as one might like.
There have been many different proposed semantics of run-time type
checking: ``transient'' cast semantics~\cite{vitousekswordssiek:2017}
only checks the head connective of a type (number, function, list,
-\ldots), ``eager'' cast semantics~\cite{hermanXXspaceefficient} checks
+\ldots), ``eager'' cast semantics~\cite{herman2010spaceefficient} checks
run-time type information on closures, whereas ``lazy'' cast
semantics~\citep{findler-felleisen02} will always delay a type-check on
a function until it is called (see \cite{siek+09designspace} for eager
@@ -9224,6 +9224,11 @@ equivalence that have been developed for these
features~\cite{plotkinabadi93, dunphyphd, ahmed08:paramseal, neis09,
ahmed09:sdri}, which may lend insight into existing
proposals~\cite{siek15:mono,ahmed17,igarashipoly17}.
+%
+In particular it would be of interest to determine if the
+``monotonic'' \citep{siek15:mono} and ``proxied'' \citep{siek-taha06}
+semantics of references support relational reasoning principles of
+local state.
\iflong \paragraph{Blame}
\fi
@@ -9236,6 +9241,12 @@ never raise positive blame, so only need to be parameterized by a
negative label and downcasts never raise negative blame so only need
to be parameterized by a positive label.
%
+There is a one subtlety: since in GTT there is only one $\err$, all
+our proven (in)equations identify all blame labels.
+%
+In future work, we could instead parameterize the theory by a set of
+labels and prove a stronger, blame-aware theorem.
+%
We argue that the observation that upcasts are thunkable and downcasts
are linear is directly related to blame in that if an upcast were
\emph{not} thunkable, it should raise positive blame and if a downcast
@@ -9364,7 +9375,7 @@ accurate model of implementations of Scheme that pass multiple
arguments on the stack.
\end{longonly}
-\smallskip
+%% \smallskip
In this paper, we have given an axiomatic logic for reasoning about
gradual programs in a mixed call-by-value/call-by-name language, shown
diff --git a/paper/max.bib b/paper/max.bib
index bd52e79..6bcdd06 100644
--- a/paper/max.bib
+++ b/paper/max.bib
@@ -1140,4 +1140,11 @@ pages="396--410",
title = {Contextual Isomorphisms},
booktitle = popl,
year={2017},
-}
\ No newline at end of file
+}
+
+@article{herman2010spaceefficient,
+ title={Space-efficient gradual typing},
+ author={Herman, David and Tomb, Aaron and Flanagan, Cormac},
+ journal={Higher-Order and Symbolic Computation},
+ year={2010},
+}
--
GitLab