-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtr.tex
90 lines (71 loc) · 2.02 KB
/
tr.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
\documentclass[nonacm,review,timestamp]{acmart}
\input{package.tex}
\input{def.tex}
\title{Complete Monitoring for Gradual Types: Supplementary Material}
\author{Ben Greenman}
\orcid{0000-0001-7078-9287}
\affiliation{%
\institution{PLT @ Northeastern University}
\city{Boston}
\state{Massachusetts}
\country{USA}
}
\email{benjaminlgreenman@gmail.com}
\author{Matthias Felleisen}
\orcid{0000-0001-6678-1004}
\affiliation{%
\institution{PLT @ Northeastern University}
\city{Boston}
\state{Massachusetts}
\country{USA}
}
\email{matthias@ccs.neu.edu}
\author{Christos Dimoulas}
\orcid{0000-0002-9338-7034}
\affiliation{%
\institution{PLT @ Northwestern University}
\city{Evanston}
\state{Illinois}
\country{USA}
}
\email{chrdimo@northwestern.edu}
\renewcommand{\shortauthors}{Ben Greenman, Matthias Felleisen, and Christos Dimoulas}
\begin{document}
\begin{abstract}
Key concepts:
path-based ownership (\nsym~\ref{sec:N:path-based}, \tsym~\ref{sec:T:path-based}, \asym~\ref{sec:A:path-based}),
heap-based ownership (\tsym~\ref{sec:heap-based}),
type soundness (\nsym~\ref{H-S-type-soundness}, \asym~\ref{A-S-type-soundness}, \tsym~\ref{T-S-type-soundness}),
complete monitoring (\nsym~\ref{H-S-complete-monitoring}),
blame soundness + completeness (\nsym~\ref{H-S-correct-blame}, \asym~\ref{A-correct-blame}),
heap-based blame soundness (\tsym~\ref{T-all-path-blame-soundness}).
\end{abstract}
\maketitle
\tableofcontents
\section{Common Definitions}
\input{tr-common.tex}
\newpage
\section{\Nname{}}
\input{tr-N.tex}
\newpage
\section{\Tname{}}
\input{tr-T.tex}
\newpage
\section{\Aname{}}
\input{tr-A.tex}
\newpage
\section{\Nname{}\ Theorems, Lemmas, and Proofs}
\input{tr-N-proof.tex}
\newpage
\section{\Tname{}\ Theorems, Lemmas, and Proofs}
\input{tr-T-proof.tex}
\newpage
\section{\Aname{}\ Theorems, Lemmas, and Proofs}
\input{tr-A-proof.tex}
\newpage
\section{\nsym/\asym\ Simulation}
\input{tr-NA-proof.tex}
\newpage
\section{\asym/\tsym\ Simulation}
\input{tr-AT-proof.tex}
\end{document}