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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
\usepackage[outputdir=latex.out]{minted}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{xpatch,letltxmacro}
\usepackage{newunicodechar}
\usepackage{lmodern}
\usepackage{stmaryrd}
\usepackage{todo}
\usepackage{url}
\usepackage{hyperref}
\usepackage{tikz}
\usepackage{calc}
\usepackage{amssymb}
\usepackage{array}
\usepackage{wrapfig}
\usepackage[inline]{enumitem}

\newcommand{\memdom}{\fcode{AMem_dom}}
\newcommand{\neardots}{.\!.\!.}
\newcommand{\addressable}{\fcode{addressable}}





\newlist{enumi}{enumerate*}{1}
\setlist*[enumi,1]{%
  label=(\roman*),
}

\newcommand{\Arrow}[1]{%
     \parbox{#1}{\tikz{\draw[->](0,0)--(#1,0);}}
}
\newcommand{\printtowidth}[2]{\makebox[\widthof{#1}]{#2}}
\newcommand{\onecharwidth}[1]{\printtowidth{x}{#1}}
\newcommand{\twocharwidth}[1]{\printtowidth{xx}{#1}}
\newcommand{\threecharwidth}[1]{\printtowidth{xxx}{#1}}
\newcommand{\fourcharwidth}[1]{\printtowidth{xxxx}{#1}}

\newcommand{\printtowidthL}[2]{\makebox[\widthof{#1}][l]{#2}}
\newcommand{\onecharwidthL}[1]{\printtowidthL{x}{#1}}
\newcommand{\twocharwidthL}[1]{\printtowidthL{xx}{#1}}
\newcommand{\threecharwidthL}[1]{\printtowidthL{xxx}{#1}}
\newcommand{\fourcharwidthL}[1]{\printtowidthL{xxxx}{#1}}

%% \usepackage{cancel}
%% \newcommand{\notPropEq}{\twocharwidth{\cancel{\tt==}}}
\newcommand{\notPropEq}{\twocharwidth{\rlap{\hspace{1.1mm}/}\texttt{=\hspace{0.3mm}=}}}

\newunicodechar{∈}{\onecharwidth{$\in$}}
\newunicodechar{⊆}{\onecharwidth{$\subseteq$}}
\newunicodechar{⊑}{\onecharwidth{\scalebox{0.8}[0.95]{$\sqsubseteq$}}}
\newunicodechar{∪}{\onecharwidth{$\cup$}}
\newunicodechar{∩}{\onecharwidth{$\cap$}}
\newunicodechar{⊔}{\onecharwidth{$\sqcup$}}
\newunicodechar{⊓}{\onecharwidth{$\sqcap$}}
\newunicodechar{γ}{\onecharwidth{$\gamma$}}
\newunicodechar{→}{\onecharwidth{~\Arrow{.18cm}}}
\newunicodechar{⇒}{\threecharwidth{$\implies$}}
\newunicodechar{∖}{\onecharwidth{$\setminus$}}

\newunicodechar{ℤ}{\onecharwidth{$\mathbb Z$}}
\newunicodechar{ℕ}{\onecharwidth{$\mathbb N$}}
\newunicodechar{β}{\onecharwidth{$\beta$}}

\newunicodechar{ⵌ}{\onecharwidth{${{}^\#}$}}
\newunicodechar{⊕}{\onecharwidth{$\oplus$}}
% thin space
\newunicodechar{ }{\,}

\newunicodechar{⊤}{\onecharwidth{$\top$}}
\newunicodechar{⊥}{\onecharwidth{$\bot$}}
\newunicodechar{λ}{\onecharwidth{$\lambda$}}
\newunicodechar{∨}{\onecharwidth{$\vee$}}
\newunicodechar{∧}{\onecharwidth{$\wedge$}}
\newunicodechar{≠}{\onecharwidth{$\neq$}}
\newunicodechar{∃}{\onecharwidth{$\exists$}}
\newunicodechar{∀}{\onecharwidth{$\forall$}}
\newunicodechar{×}{\onecharwidth{$\times$}}
\newunicodechar{≤}{\onecharwidth{$\leq$}}
\newunicodechar{≥}{\onecharwidth{$\geq$}}
\newunicodechar{⇔}{\threecharwidth{$\iff$}}

\newunicodechar{⦇}{\onecharwidth{$\llparenthesis$}}
\newunicodechar{⦈}{\onecharwidth{$\rrparenthesis$}}

\newunicodechar{₀}{\onecharwidth{${}_0$}}
\newunicodechar{₁}{\onecharwidth{${}_1$}}
\newunicodechar{₂}{\onecharwidth{${}_2$}}
\newunicodechar{₃}{\onecharwidth{${}_3$}}
\newunicodechar{₄}{\onecharwidth{${}_4$}}
\newunicodechar{₅}{\onecharwidth{${}_5$}}
\newunicodechar{₆}{\onecharwidth{${}_6$}}
\newunicodechar{₇}{\onecharwidth{${}_7$}}
\newunicodechar{₈}{\onecharwidth{${}_8$}}
\newunicodechar{₉}{\onecharwidth{${}_9$}}
\newunicodechar{ⁿ}{\onecharwidth{${}^n$}}

\newcommand{\oneCharSub}[1]{\onecharwidth{${}_{\texttt{#1}}$}}
\newcommand{\twoCharSub}[1]{\twocharwidth{${}_{\texttt{#1}}$}}
\newcommand{\threeCharSub}[1]{\threecharwidth{${}_{\texttt{#1}}$}}
\newcommand{\fourCharSub}[1]{\fourcharwidth{${}_{\texttt{#1}}$}}
\newcommand{\oneCharSubExp}[2]{\onecharwidth{${}_{\texttt{#1}}^{\texttt{#2}}$}}

\newcommand{\oneCharSubL}[1]{\onecharwidthL{${}_{\texttt{#1}}$}}
\newcommand{\twoCharSubL}[1]{\twocharwidthL{${}_{\texttt{#1}}$}}
\newcommand{\threeCharSubL}[1]{\threecharwidthL{${}_{\texttt{#1}}$}}
\newcommand{\fourCharSubL}[1]{\fourcharwidthL{${}_{\texttt{#1}}$}}
\newcommand{\oneCharSubExpL}[2]{\onecharwidthL{${}_{\texttt{#1}}^{\texttt{#2}}$}}

\newcommand{\oneCharSubD}[1]{\onecharwidth{${}^\#_{\texttt{#1}}$}}
\newcommand{\twoCharSubD}[1]{\twocharwidth{${}^\#_{\texttt{#1}}$}}
\newcommand{\threeCharSubD}[1]{\threecharwidth{${}^\#_{\texttt{#1}}$}}
\newcommand{\fourCharSubD}[1]{\fourcharwidth{${}^\#_{\texttt{#1}}$}}

\newcommand{\oneCharSubLD}[1]{\onecharwidthL{${}^\#_{\texttt{#1}}$}}
\newcommand{\twoCharSubLD}[1]{\twocharwidthL{${}^\#_{\texttt{#1}}$}}
\newcommand{\threeCharSubLD}[1]{\threecharwidthL{${}^\#_{\texttt{#1}}$}}
\newcommand{\fourCharSubLD}[1]{\fourcharwidthL{${}^\#_{\texttt{#1}}$}}


\makeatletter
\AtBeginEnvironment{minted}{\dontdofcolorbox}
\def\dontdofcolorbox{\renewcommand\fcolorbox[4][]{##4}}
\xpatchcmd{\inputminted}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{}
\xpatchcmd{\mintinline}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{} % see https://tex.stackexchange.com/a/401250/
\makeatother

\input{latex/glossary.tex}
\input{latex/commands.tex}

\def\IMP{\textrm{IMP}}








%% \title{A formally verified abstract interpreter written in F*}
\title{Verified Functional Programming \\of an Abstract Interpreter}

%% \author{First Author\inst{1} \and
%% Second Author\inst{2,3} \and
%% Third Author\inst{3}}