From 5a6026a20215fe3296dc114525618d08fac61bf0 Mon Sep 17 00:00:00 2001 From: Dan Licata <drl@cs.cmu.edu> Date: Mon, 9 Jul 2018 12:43:40 -0400 Subject: [PATCH] edits --- paper/gtt.tex | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/paper/gtt.tex b/paper/gtt.tex index c0549c3..c98b92b 100644 --- a/paper/gtt.tex +++ b/paper/gtt.tex @@ -7019,7 +7019,7 @@ $x$ exactly once, first, these two are the same. \] \end{definition} Thunkability/linearity of the translations of complex values/stacks are -useed to prove the preservation of the $\eta$ principles for positive +used to prove the preservation of the $\eta$ principles for positive types and the strictness of complex stacks with respect to errors under decomplexification. @@ -7303,6 +7303,10 @@ morphisms from smaller ones. \end{enumerate} \end{longproof} +Composing this with the previous translation from GTT to \cbpvstar\/ +shows that \emph{GTT value type upcasts are thunkable and computation + type downcasts are linear}. + \begin{longonly} Since the translation takes values and stacks to terms, it cannot -- GitLab