-
Notifications
You must be signed in to change notification settings - Fork 0
/
paper.tex
109 lines (88 loc) · 3.76 KB
/
paper.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
\documentclass[acmsmall, screen]{acmart}
%% NOTES among authors
%\def\notes#1{\expandafter\def\csname#1\endcsname##1{\marginpar{\par\noindent\hrulefill\par\raggedright\tiny\noindent #1: ##1}}}
%% \def\notes#1{\expandafter\def\csname#1\endcsname##1{\marginpar{\relax}}}
%\notes{bg}
%\notes{cd}
%\notes{mf}
\title{Complete Monitors for Gradual Types}
\author{Ben Greenman}
\orcid{0000-0001-7078-9287}
\affiliation{%
\institution{PLT @ Northeastern University}
\city{Boston}
\state{Massachusetts}
\country{USA}
}
\email{[email protected]}
\author{Matthias Felleisen}
\orcid{0000-0001-6678-1004}
\affiliation{%
\institution{PLT @ Northeastern University}
\city{Boston}
\state{Massachusetts}
\country{USA}
}
\email{[email protected]}
\author{Christos Dimoulas}
\orcid{0000-0002-9338-7034}
\affiliation{%
\institution{PLT @ Northwestern University}
\city{Evanston}
\state{Illinois}
\country{USA}
}
\email{[email protected]}
\renewcommand{\shortauthors}{Ben Greenman, Matthias Felleisen, and Christos Dimoulas}
\input{package.tex}
\input{def.tex}
%%% The following is specific to OOPSLA '19 and the paper
%%% 'Complete Monitors for Gradual Types'
%%% by Ben Greenman, Matthias Felleisen, and Christos Dimoulas.
\setcopyright{acmcopyright}
\acmJournal{PACMPL}
\acmYear{2019} \acmVolume{3} \acmNumber{OOPSLA} \acmArticle{122} \acmMonth{10} \acmPrice{} \acmDOI{10.1145/3360548}
\copyrightyear{2019}
\citestyle{acmauthoryear}
\begin{document}
\begin{abstract}
\input{abstract.tex}
\end{abstract}
\begin{CCSXML}
\input{ccsxml.tex}
\end{CCSXML}
\ccsdesc[500]{Software and its engineering~Semantics}
\ccsdesc[100]{Software and its engineering~Constraints}
\ccsdesc[100]{Software and its engineering~Functional languages}
\keywords{complete monitoring, blame soundness, blame completeness}
\maketitle
\def\sec#1#2#3{\section{#1} \label{#2} \input{#3}}
%% title label file
%% ---------------------------------------------------------------------------------------------------
\sec{Type Soundness Is Not Enough} {sec:intro} {introduction}
\sec{Motivational Examples, the Basic Insights} {sec:motivation} {motivation}
\sec{The Model: Syntax and Types} {sec:surface} {surface}
\sec{The Model: Three Semantics} {sec:semantics} {semantics}
\sec{Type Soundness} {sec:soundness} {soundness}
\sec{Type Soundness Is {\em Really\/} Not Enough} {sec:not} {not-soundness}
\sec{Ownership: Labels and Reductions} {sec:ownership} {ownership}
\sec{Complete Monitoring} {sec:satisfies} {satisfies}
\sec{Implications for Blame} {sec:blame} {blame}
\sec{Related Work} {sec:related} {related}
\sec{Complete Monitoring Is Needed} {sec:conclusion} {conclusion}
\begin{acks}
We thank Michael M. Vitousek for conversations about Transient and its type soundness;
% "However, I don't think the soundness we guarantee is fundamentally different from soundness in Typed Racket; at
% least, the places where behavior differs are few." -- Mike V.
Amal Ahmed, Michael Ballantyne, Stephen Chang, and Max S. New for
conversations about complete monitoring;
and the anonymous OOPSLA reviewers for their questions, comments, and proofreading.
This work was partially supported by \grantsponsor{NSF}{NSF}{https://www.nsf.gov}
grants
\href{"https://www.nsf.gov/awardsearch/showAward?AWD_ID=1518844"}{\grantnum{NSF}{CCF 1518844}}
and
\href{"https://www.nsf.gov/awardsearch/showAward?AWD_ID=1763922"}{\grantnum{NSF}{CCF 1763922}}.
\end{acks}
\bibliographystyle{ACM-Reference-Format}
\bibliography{bib,cs}
\end{document}