From ae86766df9f3279b8acecebff7c824d53f9204b8 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Mon, 5 Nov 2018 18:09:32 -0500
Subject: [PATCH] add in copyright and classification stuff, hack one sentence
to get it in perfect space
---
paper/gtt.tex | 55 ++++++++++++++++++++++-----------------------------
1 file changed, 24 insertions(+), 31 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index a83e33c..b3b1ac7 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -29,15 +29,10 @@
%%% 'Gradual Type Theory'
%%% by Max S. New, Daniel R. Licata, and Amal Ahmed.
%%%
-\acmPrice{}
-\acmDOI{10.1145/3290328}
-\acmYear{2019}
-\copyrightyear{2019}
+
+\setcopyright{rightsretained}
\acmJournal{PACMPL}
-\acmVolume{3}
-\acmNumber{POPL}
-\acmArticle{15}
-\acmMonth{1}
+\acmYear{2019} \acmVolume{3} \acmNumber{POPL} \acmArticle{15} \acmMonth{1} \acmPrice{}\acmDOI{10.1145/3290328}
%% Copyright information
%% Supplied to authors (based on authors' rights management selection;
@@ -283,30 +278,29 @@
%% 2012 ACM Computing Classification System (CSS) concepts
%% Generate at 'http://dl.acm.org/ccs/ccs.cfm'.
-%% TODO
-%% \begin{CCSXML}
-%% <ccs2012>
-%% <concept>
-%% <concept_id>10011007.10011006.10011008</concept_id>
-%% <concept_desc>Software and its engineering~General programming languages</concept_desc>
-%% <concept_significance>500</concept_significance>
-%% </concept>
-%% <concept>
-%% <concept_id>10003456.10003457.10003521.10003525</concept_id>
-%% <concept_desc>Social and professional topics~History of programming languages</concept_desc>
-%% <concept_significance>300</concept_significance>
-%% </concept>
-%% </ccs2012>
-%% \end{CCSXML}
-
-%% \ccsdesc[500]{Software and its engineering~General programming languages}
-%% \ccsdesc[300]{Social and professional topics~History of programming languages}
+ \begin{CCSXML}
+<ccs2012>
+<concept>
+<concept_id>10003752.10010124.10010131.10010135</concept_id>
+<concept_desc>Theory of computation~Axiomatic semantics</concept_desc>
+<concept_significance>500</concept_significance>
+</concept>
+<concept>
+<concept_id>10011007.10011006.10011008.10011009.10011012</concept_id>
+<concept_desc>Software and its engineering~Functional languages</concept_desc>
+<concept_significance>500</concept_significance>
+</concept>
+</ccs2012>
+\end{CCSXML}
+
+\ccsdesc[500]{Theory of computation~Axiomatic semantics}
+\ccsdesc[500]{Software and its engineering~Functional languages}
%% End of generated code
%% Keywords
%% comma separated list
-% \keywords{keyword1, keyword2, keyword3} %% \keywords is optional
+\keywords{gradual typing, graduality, call-by-push-value}
%% \maketitle
@@ -9337,8 +9331,8 @@ $\errordivergerightop$ gives
$\Gamma \pipe \Delta \vDash E' \ix{\mathrel{\preceq\gtdyn}} \omega E \in \u B$.
\end{lemma}
-Because logical equivalence implies contextual equivalence, we can
-then conclude with the main theorem:
+Because logical implies contextual equivalence, we can
+conclude with the main theorem:
\begin{theorem}[Contextual Approximation/Equivalence Model CBPV] ~~\\
If $\Gamma \pipe \Delta \vdash E \ltdyn E' : T$ then
$\Gamma \pipe \Delta \vDash E \ctxize\ltdyn E' \in T$;
@@ -9773,13 +9767,12 @@ structure~\cite{ahman+16fiberedeffects}.
%% \newpage
\paragraph{Acknowledgments}
-
We thank Ron Garcia, Kenji Maillard and Gabriel Scherer for helpful
discussions about this work. We thank the anonymous reviewers for
helpful feedback on this article. This material is based on research
sponsored by the National Science Foundation under grant CCF-1453796
and the United States Air Force Research Laboratory under agreement
-number FA9550-15-1-0053 and and FA9550-16-1-0292.
+number FA9550-15-1-0053 and FA9550-16-1-0292.
%% The U.S. Government is
%% authorized to reproduce and distribute reprints for Governmental
%% purposes notwithstanding any copyright notation thereon.
--
GitLab