From d0de6fb8f2a9a4513745f5e6c6da1cde89259d63 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Mon, 5 Nov 2018 15:32:29 -0500
Subject: [PATCH] long version stuff and a typo
---
paper/acmart.cls | 160 +++++++++++++++++++++++++++++++----------------
paper/gtt.tex | 52 +++++++--------
2 files changed, 129 insertions(+), 83 deletions(-)
diff --git a/paper/acmart.cls b/paper/acmart.cls
index e10b463..403b13f 100644
--- a/paper/acmart.cls
+++ b/paper/acmart.cls
@@ -37,8 +37,14 @@
%% Right brace \} Tilde \~}
\NeedsTeXFormat{LaTeX2e}
\ProvidesClass{acmart}
-[2018/04/14 v1.53 Typesetting articles for the Association for
-Computing Machinery]
+[2018/05/09 v1.54 Typesetting articles for the Association for
+Computing Machinery, modified to add a 'nonacm' option -- see
+ https://github.com/borisveytsman/acmart/pull/282.
+You may obtain the source of this modified version at
+ https://github.com/gasche/acmart/blob/nonacm-derived/acmart.dtx,
+and the original version at
+ https://github.com/borisveytsman/acmart/.
+]
\def\@classname{acmart}
\InputIfFileExists{acmart-preload-hook.tex}{%
\ClassWarning{\@classname}{%
@@ -96,6 +102,18 @@ Computing Machinery]
\fi}{\PackageError{\@classname}{The option authorversion can be either true or
false}}
\ExecuteOptionsX{authorversion=false}
+\define@boolkey+{acmart.cls}[@ACM@]{nonacm}[true]{%
+ \if@ACM@nonacm
+ \PackageInfo{\@classname}{Using nonacm mode}%
+ \AtBeginDocument{\@ACM@printacmreffalse}%
+ % in 'nonacm' mode we disable the "ACM Reference Format"
+ % printing by default, but this can be re-enabled by the
+ % user using \settopmatter{printacmref=true}
+ \else
+ \PackageInfo{\@classname}{Not using nonacm mode}%
+ \fi}{\PackageError{\@classname}{The option nonacm can be either true or
+ false}}
+\ExecuteOptionsX{nonacm=false}
\define@boolkey+{acmart.cls}[@ACM@]{natbib}[true]{%
\if@ACM@natbib
\PackageInfo{\@classname}{Explicitly selecting natbib mode}%
@@ -1606,7 +1624,7 @@ Computing Machinery]
\fi
\fi
\fi
- \footnotetextcopyrightpermission{%
+ \if@ACM@nonacm\else\footnotetextcopyrightpermission{%
\if@ACM@authordraft
\raisebox{-2ex}[\z@][\z@]{\makebox[0pt][l]{\large\bfseries
Unpublished working draft. Not for distribution.}}%
@@ -1624,7 +1642,7 @@ Computing Machinery]
\if@printcopyright
\copyright\ \@copyrightyear\ \@copyrightowner\\
\else
- \@copyrightyear.\
+ \@copyrightyear.\
\fi
\if@ACM@manuscript
Manuscript submitted to ACM\\
@@ -1644,17 +1662,20 @@ Computing Machinery]
, \@formatdoi{\@acmDOI}.
\fi\\
\else
- \if@ACM@journal
- \@permissionCodeOne/\@acmYear/\@acmMonth-ART\@acmArticle
- \ifx\@acmPrice\@empty\else\ \$\@acmPrice\fi\\
- \@formatdoi{\@acmDOI}%
- \else % Conference
- \ifx\@acmISBN\@empty\else ACM~ISBN~\@acmISBN
- \ifx\@acmPrice\@empty.\else\dots\$\@acmPrice\fi\\\fi
- \ifx\@acmDOI\@empty\else\@formatdoi{\@acmDOI}\fi%
+ \if@ACM@nonacm\else
+ \if@ACM@journal
+ \@permissionCodeOne/\@acmYear/\@acmMonth-ART\@acmArticle
+ \ifx\@acmPrice\@empty\else\ \$\@acmPrice\fi\\
+ \@formatdoi{\@acmDOI}%
+ \else % Conference
+ \ifx\@acmISBN\@empty\else ACM~ISBN~\@acmISBN
+ \ifx\@acmPrice\@empty.\else\dots\$\@acmPrice\fi\\\fi
+ \ifx\@acmDOI\@empty\else\@formatdoi{\@acmDOI}\fi%
+ \fi
\fi
\fi
\fi}
+ \fi
\endgroup
\setcounter{footnote}{0}%
\@mkabstract
@@ -2143,7 +2164,7 @@ Computing Machinery]
\def\@pages@word{\ifnum\getrefnumber{TotPages}=1\relax page\else pages\fi}%
\def\footnotemark{}%
\def\\{\unskip{} \ignorespaces}%
- \def\footnote{\ClassError{\@classname}{Please do note use footnotes
+ \def\footnote{\ClassError{\@classname}{Please do not use footnotes
inside a \string\title{} or \string\author{} command! Use
\string\titlenote{} or \string\authornote{} instead!}}%
\def\@article@string{\ifx\@acmArticle\@empty{\ }\else,
@@ -2151,17 +2172,23 @@ Computing Machinery]
\par\medskip\small\noindent{\bfseries ACM Reference Format:}\par\nobreak
\noindent\authors. \@acmYear. \@title
\ifx\@subtitle\@empty. \else: \@subtitle. \fi
- \if@ACM@journal
- \textit{\@journalNameShort}
- \@acmVolume, \@acmNumber \@article@string (\@acmPubDate),
- \ref{TotPages}~\@pages@word.
- \else
- In \textit{\@acmBooktitle}%
- \ifx\@acmEditors\@empty\textit{.}\else
- \andify\@acmEditors\textit{, }\@acmEditors~\@editorsAbbrev.%
- \fi\
- ACM, New York, NY, USA%
- \@article@string\unskip, \ref{TotPages}~\@pages@word.
+ \if@ACM@nonacm\else
+ % The 'nonacm' option disables 'printacmref' by default,
+ % and the present \@mkbibcitation definition is never used
+ % in this case. The conditional remains useful if the user
+ % explicitly sets \settopmatter{printacmref=true}.
+ \if@ACM@journal
+ \textit{\@journalNameShort}
+ \@acmVolume, \@acmNumber \@article@string (\@acmPubDate),
+ \ref{TotPages}~\@pages@word.
+ \else
+ In \textit{\@acmBooktitle}%
+ \ifx\@acmEditors\@empty\textit{.}\else
+ \andify\@acmEditors\textit{, }\@acmEditors~\@editorsAbbrev.%
+ \fi\
+ ACM, New York, NY, USA%
+ \@article@string\unskip, \ref{TotPages}~\@pages@word.
+ \fi
\fi
\ifx\@acmDOI\@empty\else\@formatdoi{\@acmDOI}\fi
\par\egroup}
@@ -2221,45 +2248,62 @@ Computing Machinery]
\fancyhf{}%
\renewcommand{\headrulewidth}{\z@}%
\renewcommand{\footrulewidth}{\z@}%
+ \def\@acmArticlePage{%
+ \ifx\@acmArticle\empty%
+ \if@ACM@printfolios\thepage\fi%
+ \else%
+ \@acmArticle\if@ACM@printfolios:\thepage\fi%
+ \fi%
+ }
\ifcase\ACM@format@nr
\relax % manuscript
\fancyhead[LE]{\ACM@linecountL\if@ACM@printfolios\thepage\fi}%
\fancyhead[RO]{\if@ACM@printfolios\thepage\fi}%
\fancyhead[RE]{\@shortauthors}%
\fancyhead[LO]{\ACM@linecountL\shorttitle}%
- \fancyfoot[RO,LE]{\footnotesize Manuscript submitted to ACM}%
+ \if@ACM@nonacm\else%
+ \fancyfoot[RO,LE]{\footnotesize Manuscript submitted to ACM}
+ \fi%
\or % acmsmall
- \fancyhead[LE]{\ACM@linecountL\@headfootfont\@acmArticle\if@ACM@printfolios:\thepage\fi}%
- \fancyhead[RO]{\@headfootfont\@acmArticle\if@ACM@printfolios:\thepage\fi}%
+ \fancyhead[LE]{\ACM@linecountL\@headfootfont\@acmArticlePage}%
+ \fancyhead[RO]{\@headfootfont\@acmArticlePage}%
\fancyhead[RE]{\@headfootfont\@shortauthors}%
\fancyhead[LO]{\ACM@linecountL\@headfootfont\shorttitle}%
- \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
- \@acmNumber, Article \@acmArticle. Publication date: \@acmPubDate.}%
+ \if@ACM@nonacm\else%
+ \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
+ \@acmNumber, Article \@acmArticle. Publication date: \@acmPubDate.}%
+ \fi%
\or % acmlarge
\fancyhead[LE]{\ACM@linecountL\@headfootfont
- \@acmArticle\if@ACM@printfolios:\thepage\fi\quad\textbullet\quad\@shortauthors}%
+ \@acmArticlePage\quad\textbullet\quad\@shortauthors}%
\fancyhead[LO]{\ACM@linecountL}%
\fancyhead[RO]{\@headfootfont
- \shorttitle\quad\textbullet\quad\@acmArticle\if@ACM@printfolios:\thepage\fi}%
- \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
- \@acmNumber, Article \@acmArticle. Publication date: \@acmPubDate.}%
+ \shorttitle\quad\textbullet\quad\@acmArticlePage}%
+ \if@ACM@nonacm\else%
+ \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
+ \@acmNumber, Article \@acmArticle. Publication date: \@acmPubDate.}%
+ \fi%
\or % acmtog
\fancyhead[LE]{\ACM@linecountL\@headfootfont
- \@acmArticle\if@ACM@printfolios:\thepage\fi\quad\textbullet\quad\@shortauthors}%
+ \@acmArticlePage\quad\textbullet\quad\@shortauthors}%
\fancyhead[LO]{\ACM@linecountL}%
\fancyhead[RE]{\ACM@linecountR}%
\fancyhead[RO]{\@headfootfont
- \shorttitle\quad\textbullet\quad\@acmArticle\if@ACM@printfolios:\thepage\fi\ACM@linecountR}%
- \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
- \@acmNumber, Article \@acmArticle. Publication date: \@acmPubDate.}%
+ \shorttitle\quad\textbullet\quad\@acmArticlePage\ACM@linecountR}%
+ \if@ACM@nonacm\else%
+ \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
+ \@acmNumber, Article \@acmArticle. Publication date: \@acmPubDate.}%
+ \fi%
\else % Proceedings
\fancyfoot[C]{\if@ACM@printfolios\footnotesize\thepage\fi}%
\fancyhead[LO]{\ACM@linecountL\@headfootfont\shorttitle}%
\fancyhead[RE]{\@headfootfont\@shortauthors\ACM@linecountR}%
- \fancyhead[LE]{\ACM@linecountL\@headfootfont\acmConference@shortname,
- \acmConference@date, \acmConference@venue}%
- \fancyhead[RO]{\@headfootfont\acmConference@shortname,
- \acmConference@date, \acmConference@venue\ACM@linecountR}%
+ \if@ACM@nonacm\else%
+ \fancyhead[LE]{\ACM@linecountL\@headfootfont\acmConference@shortname,
+ \acmConference@date, \acmConference@venue}%
+ \fancyhead[RO]{\@headfootfont\acmConference@shortname,
+ \acmConference@date, \acmConference@venue\ACM@linecountR}%
+ \fi%
\fi
\if@ACM@sigchiamode
\fancyheadoffset[L]{\dimexpr(\marginparsep+\marginparwidth)}%
@@ -2317,27 +2361,35 @@ Computing Machinery]
\relax % manuscript
\fancyhead[L]{\ACM@linecountL}%
\fancyfoot[RO,LE]{\if@ACM@printfolios\small\thepage\fi}%
- \fancyfoot[RE,LO]{\footnotesize Manuscript submitted to ACM}%
+ \if@ACM@nonacm\else%
+ \fancyfoot[RE,LO]{\footnotesize Manuscript submitted to ACM}%
+ \fi%
\or % acmsmall
- \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
- \@acmNumber, Article \@acmArticle. Publication date:
- \@acmPubDate.}%
+ \if@ACM@nonacm\else%
+ \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
+ \@acmNumber, Article \@acmArticle. Publication date:
+ \@acmPubDate.}%
+ \fi%
\fancyhead[LE]{\ACM@linecountL\@folioblob}%
\fancyhead[LO]{\ACM@linecountL}%
\fancyhead[RO]{\@folioblob}%
\fancyheadoffset[RO,LE]{0.6\@folio@wd}%
\or % acmlarge
- \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
- \@acmNumber, Article \@acmArticle. Publication date:
- \@acmPubDate.}%
+ \if@ACM@nonacm\else%
+ \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
+ \@acmNumber, Article \@acmArticle. Publication date:
+ \@acmPubDate.}%
+ \fi%
\fancyhead[RO]{\@folioblob}%
\fancyhead[LE]{\ACM@linecountL\@folioblob}%
\fancyhead[LO]{\ACM@linecountL}%
\fancyheadoffset[RO,LE]{1.4\@folio@wd}%
\or % acmtog
- \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
- \@acmNumber, Article \@acmArticle. Publication date:
- \@acmPubDate.}%
+ \if@ACM@nonacm\else%
+ \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
+ \@acmNumber, Article \@acmArticle. Publication date:
+ \@acmPubDate.}%
+ \fi%
\fancyhead[L]{\ACM@linecountL}%
\fancyhead[R]{\ACM@linecountR}%
\else % Conference proceedings
@@ -2348,7 +2400,9 @@ Computing Machinery]
\if@ACM@timestamp
\ifnum\ACM@format@nr=0\relax % Manuscript
\fancyfoot[LO,RE]{\ACM@timestamp\quad
- \footnotesize Manuscript submitted to ACM}
+ \if@ACM@nonacm\else
+ \footnotesize Manuscript submitted to ACM
+ \fi}
\else
\fancyfoot[LO,RE]{\ACM@timestamp}
\fi
@@ -2583,4 +2637,4 @@ Computing Machinery]
\normalsize\normalfont\frenchspacing
\endinput
%%
-%% End of file `acmart.cls'.
\ No newline at end of file
+%% End of file `acmart.cls'.
diff --git a/paper/gtt.tex b/paper/gtt.tex
index e4ece66..e94420b 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1,20 +1,15 @@
-%% For double-blind review submission, w/o CCS and ACM Reference (max submission space)
-%% \documentclass[acmsmall,review,anonymous]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
-%% For double-blind review submission, w/ CCS and ACM Reference
-%\documentclass[acmsmall,review,anonymous]{acmart}\settopmatter{printfolios=true}
-%% For single-blind review submission, w/o CCS and ACM Reference (max submission space)
-%\documentclass[acmsmall,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
-%% For single-blind review submission, w/ CCS and ACM Reference
-%\documentclass[acmsmall,review]{acmart}\settopmatter{printfolios=true}
-%% For final camera-ready submission, w/ required CCS and ACM Reference
-\documentclass[acmsmall]{acmart}\settopmatter{}
-
\newif\ifshort
\newif\iflong
%% Pick long or short version:
\shorttrue
%% \longtrue
+%% For final camera-ready submission, w/ required CCS and ACM Reference
+\ifshort\documentclass[acmsmall,screen]{acmart}\settopmatter{}\fi
+%% For
+\iflong\documentclass[acmsmall,nonacm]{acmart}\fi
+
+
%% Note: Authors migrating a paper from PACMPL format to traditional
%% SIGPLAN proceedings format should change 'acmlarge' to
%% 'sigplan,10pt'.
@@ -31,26 +26,20 @@
% \usepackage{subcaption} %% For complex figures with subfigures/subcaptions
% %% http://ctan.org/pkg/subcaption
-\makeatletter\if@ACM@journal\makeatother
-%% Journal information (used by PACMPL format)
-%% Supplied to authors by publisher for camera-ready submission
+%%% The following is specific to POPL '19 and the paper
+%%% 'Gradual Type Theory'
+%%% by Max S. New, Daniel R. Licata, and Amal Ahmed.
+%%%
+\acmPrice{}
+\acmDOI{10.1145/3290328}
+\acmYear{2019}
+\copyrightyear{2019}
\acmJournal{PACMPL}
-\acmVolume{1}
-\acmNumber{1}
-\acmArticle{1}
-\acmYear{2017}
+\acmVolume{3}
+\acmNumber{POPL}
+\acmArticle{15}
\acmMonth{1}
-\acmDOI{10.1145/nnnnnnn.nnnnnnn}
-\startPage{1}
-\else\makeatother
-%% Conference information (used by SIGPLAN proceedings format)
-%% Supplied to authors by publisher for camera-ready submission
-\acmConference[PL'17]{ACM SIGPLAN Conference on Programming Languages}{January 01--03, 2017}{New York, NY, USA}
-\acmYear{2017}
-\acmISBN{978-x-xxxx-xxxx-x/YY/MM}
-\acmDOI{10.1145/nnnnnnn.nnnnnnn}
-\startPage{1}
-\fi
+
%% Copyright information
%% Supplied to authors (based on authors' rights management selection;
%% see authors.acm.org) by publisher for camera-ready submission
@@ -7822,7 +7811,7 @@ in figure
S[\caseofXthenYelseZ{\inl V}{x_1. M_1}{x_2. M_2}] &\stepzero & S[M_1[V/x_1]]\\
S[\caseofXthenYelseZ{\inr V}{x_1. M_1}{x_2. M_2}] &\stepzero & S[M_2[V/x_2]]\\
\fi
- S[\pmpairWtoXYinZ{(V_1,V_2)}{x_1}{x_2}{M} &\stepzero & S[M[V_1/x_1,V_2/x_2]]]\\
+ S[\pmpairWtoXYinZ{(V_1,V_2)}{x_1}{x_2}{M}] &\stepzero & S[M[V_1/x_1,V_2/x_2]]\\
S[\pmmuXtoYinZ{\rollty A V}{x}{M}] &\stepone & S[M[V/x]]\\
S[\force\thunk M] &\stepzero & S[M]\\
\iflong
@@ -9483,6 +9472,7 @@ With this embedding and the uniqueness theorem, GTT produces a
definition for lazy casts, and the definition matches the work of
\citet{XuPJC09} when restricting to non-dependent contracts.
+\iflong\paragraph{Comparing Soundness Principles for Cast Semantics}\fi
\citet{greenmanfelleisen:2018} gives a spectrum of
differing syntactic type soundness theorems for different semantics of
gradual typing.
@@ -9532,6 +9522,8 @@ satisfy the restricted $\eta$ principle provided by the language, and
so it must be graduality, and therefore meaning preservation that
fails.
+\iflong\paragraph{Axiomatic Casts}\fi
+
Henglein's work on dynamic typing also uses an axiomatic semantics of
casts, but axiomatizes behavior of casts at each type directly whereas
we give a uniform definition of all casts and derive implementations
--
GitLab