\NeedsTeXFormat{LaTeX2e} \ProvidesPackage{setup}[2018/04/25 v0.1] \newcommand\hmmax{0} \newcommand\bmmax{0} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Packages %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \let\Bbbk\relax %\usepackage{amsmath} \usepackage{mathtools} %\usepackage{amssymb} %\usepackage{amsthm} \usepackage{alltt} \usepackage{bm} \usepackage{nicefrac} %\usepackage{stmaryrd} \usepackage{mathpartir} \usepackage{color} \usepackage{listings} \usepackage[shortlabels]{enumitem} \definecolor{darkblue}{rgb}{0,0.2,0.4} %\definecolor{darkred}{rgb}{0.7,0.4,0.4} \definecolor{darkred}{rgb}{0.8,0.2,0.2} \ifwithcomments \newcommand{\ignore}[1]{{\color{red}\textbf{DELETED:}#1}} \newcommand{\beppe}[1]{{\bf\color{blue}Beppe: #1}} \newcommand{\mick}[1]{{\bf\color{gray}Mickael: #1}} \newcommand{\kim}[1]{{\bf\color{pink}Kim: #1}} \newcommand{\victor}[1]{{\bf\color{purple}Victor: #1}} \else \newcommand{\ignore}[1]{} \newcommand{\beppe}[1]{} \newcommand{\mick}[1]{} \newcommand{\kim}[1]{} \newcommand{\victor}[1]{} \fi %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Style dependend definitions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \ifelsevierstyle \newcommand{\Appendix}{} \else \newcommand{\Appendix}{Appendix } \fi \newcommand{\svvspace}[1]{ \iflongversion\else\vspace{#1}\fi } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Support macros %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand {\DeclareMyOperator}[2] {% \expandafter\newcommand\csname#1\endcsname{\textsf{\textup{#2}}}} \DeclareMathAlphabet {\MyMathBb} {U} {bbold} {m} {n} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Inference rules %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \def \TirNameStyle #1{\small #1} \newcommand {\Infer} [4] [] { \inferrule*[% left={\ifx\\#1\\#1\else\ifx\\#2\\[\textsc{#1}]\:\else[\textsc{#1}]\fi\fi},% right={$#4$}% ]% {#2}{#3}} \newcommand {\Rule}[1] {[\textsc{#1}]} \newcommand{\tcase}[4]{\ensuremath{(#1{\in}#2)\,\texttt{\textup{?}}\,#3\,\texttt{\textup{:}}\,#4}} \newcommand{\letexp}[3]{\ensuremath{\texttt{\textup{let}}\,#1\,\texttt{\textup{=}}\,#2\,\texttt{\textup{in}}\,#3\,}} \newcommand{\morecompact}{\baselineskip=9.5pt} \newcommand {\Pd} {\mathcal{P}} \newcommand {\Pf} {\mathcal{P}_{\!\textup{fin}}} \newcommand {\Domain} {\mathcal{D}} \newcommand {\Constants} {\mathcal{C}} \newcommand {\TypeInter}[1] {\llbracket #1 \rrbracket} \def\dbar{{\mkern3mu\mathchar'26\mkern-7mu\raisebox{-.7pt}{$\mathchar'26$}\mkern-11mu d}} \newcommand {\domega} {\partial} %possibilities: \dbar \dh \dj \delta \newcommand {\Set}[1] {\{#1\}} \newcommand {\ConstantsInBasicType} {\mathbb{B}} \newcommand{\tauUp}{\tau^\Uparrow} \newcommand{\sigmaUp}{\sigma^\Uparrow} \newcommand{\types}{\textbf{\textup{Types}}} \newcommand{\occ}[2]{#1{\downarrow}#2} \newcommand{\basic}[1]{\text{\fontshape{\itdefault}\fontseries{\bfdefault}\selectfont b}_{#1}} \newcommand{\tyof}[2]{\textsf{\textup{typeof}}_{#2}(#1)} \newcommand{\typof}[1]{\textsf{\textup{typeof}}(#1)} \newcommand{\typep}[3]{\textsf{\textup{Constr}}^{#1}_{#3}(#2)} \newcommand{\Gp}[2]{\textsf{Env}^{#1}_{#2}} \newcommand{\ite}[4]{\ensuremath{\texttt{if}\;#1\in#2\;\texttt{then}\;#3\;\texttt{else}\;#4}} \newcommand{\Let}[3]{\ensuremath{\texttt{let}\;#1\;\texttt{=}\;#2\;\texttt{in}\;#3}} \newcommand{\anns}{\ensuremath{A}} \newcommand{\ann}[2]{#1{\triangleright}#2} \newcommand{\alt}{~|~} \newcommand{\arrow}[2]{#1\to #2} \newcommand{\pair}[2]{#1\times #2} \newcommand{\orecord}[1]{\pmb{\texttt{\{}}#1\ {\large\textbf{..}}\pmb{\texttt{\}}}} \newcommand{\crecord}[1]{\pmb{\texttt{\{}}#1\pmb{\texttt{\}}}} \newcommand{\erecord}[1]{\texttt{\{}#1\texttt{\}}} \newcommand{\record}[2]{\{#1 ,\ \_ = #2\}} \DeclareFontFamily{U}{mathb}{} \DeclareFontShape{U}{mathb}{m}{n}{ <-5.5> mathb5 <5.5-6.5> mathb6 <6.5-7.5> mathb7 <7.5-8.5> mathb8 <8.5-9.5> mathb9 <9.5-11.5> mathb10 <11.5-> mathb12 }{} \DeclareSymbolFont{mathb}{U}{mathb}{m}{n} \DeclareMathSymbol{\sqdot}{\mathbin}{mathb}{"0D}% name to be checked \newcommand{\Cx}{\mathcal{C}} \newcommand{\worra}[2]{#1\mathop{\,\sqdot\,} #2} \newcommand{\apply}[2]{#1\circ#2} \newcommand {\Empty} {\ensuremath{\MyMathBb{0}}} \newcommand {\Any} {\ensuremath{\MyMathBb{1}}} \newcommand {\dom}[1]{\textsf{dom}(#1)} \newcommand {\Keyw} [1] {\text{\textsf{#1}}} \newcommand {\False} {\Keyw{False}} \newcommand {\True} {\Keyw{True}} \newcommand {\Int} {\Keyw{Int}} \newcommand {\Bool} {\Keyw{Bool}} \newcommand {\Char} {\Keyw{Char}} \newcommand {\Real} {\Keyw{Real}} \newcommand {\Complex} {\Keyw{Complex}} \newcommand {\String} {\Keyw{String}} \newcommand{\Labels}{\Keyw{Labels}} \newcommand{\Undef}{\Keyw{Undef}} \newcommand{\undefcst}{\texttt{undef}} \newcommand {\Cast}[2]{\tt #2$$\langle$$#1$$\rangle$$} \newcommand {\MCast}[2]{#2\langle #1\rangle} \newcommand {\ifty}[4]{\ensuremath{\texttt{(}#1\in#2\texttt{)?}#3\texttt{:}#4}} \newcommand {\code}[1]{\texttt{\color{darkblue}#1}} \newcommand {\p}[1]{\texttt{#1}} \newcommand {\iffdef} {\hbox{\;\;$\iff$\hspace*{-5.94mm}\raise5pt\hbox{\rm\scriptsize def}\hspace*{4mm}}} \newcommand {\eqdef} {\hbox{\;\;$=$\hspace*{-2.94mm}\raise5pt\hbox{\rm\scriptsize def}\hspace*{1mm}}} \newcommand {\eqdeftiny} {\hbox{\;\;$=$\hspace*{-2.55mm}\raise5pt\hbox{\rm\tiny def}\hspace*{1.5mm}}} \newcommand {\bpi} {\boldsymbol{\pi}} \newcommand {\bpl}[1] {\boldsymbol{\pi}_{\boldsymbol 1}(#1)} \newcommand {\bpr}[1] {\boldsymbol{\pi}_{\boldsymbol 2}(#1)} \newcommand {\proj}[2] {#2.#1} \newcommand {\recupd}[3] {\texttt{\{} #1 \texttt{ with } #2 = #3 \texttt{\}}} \newcommand {\recdel}[2] {#1 \mathtt{ \setminus } #2} \DeclareMathOperator{\eqq}{\texttt{=?}} % --------------------------------------------------------------------------------- % New packages \usepackage{bbm} % New commands \DeclarePairedDelimiter\ceil{\lceil}{\rceil} \DeclarePairedDelimiter\floor{\lfloor}{\rfloor} \newcommand{\true} {\textsf{true}} \newcommand{\false} {\textsf{false}} \newcommand{\Even} {\textsf{Even}} \newcommand{\Odd} {\textsf{Odd}} \newcommand{\subst}[2]{\{#1 \mapsto #2\}} \newcommand{\subs}[2]{\{#2/#1\}} \newcommand{\fv}{\textsf{fv}} \newcommand{\bv}{\textsf{bv}} \newcommand{\var}{\textsf{var}} \newcommand{\Refinef}{\textsf{\textup{Refine}}} \newcommand{\Refine}[2]{\ensuremath{\Refinef_{#1}(#2)}} \newcommand{\RefineStep}[1]{\textsf{\textup{RefineStep}}_{#1}} \newcommand{\constrf}{\textsf{\textup{Constr}}} \newcommand{\constr}[2]{\constrf_{#2}(#1)} %\newcommand{\env}[1]{\textsf{Env}_{#1}} \newcommand{\env}[1]{\textsf{\textup{Intertype}}_{#1}} \newcommand{\cons}[2]{{#1}\textsf{::}{#2}} \newcommand{\fixpoint}{\textsf{gfp}} \newcommand{\reduces}{\leadsto} \newcommand{\xleadsto}[1]{\overset{#1}{\leadsto}} \newcommand{\idleadsto}[0]{\xleadsto{\textit{Id}}} \newcommand{\uleadsto}[0]{\xleadsto{\large{\textbf{\_}}}} \newcommand{\values}[0]{\mathcal{V}} \newcommand{\valsemantic}[1]{{\llbracket #1 \rrbracket}_{\values}} \newcommand{\vvdash}[0]{\vdash_\values} \newcommand{\AR}{-Alg}%\ensuremath{_\mathcal{A}}} \newcommand{\eras}[1]{\lceil#1\rceil} \newcommand{\norm}[1]{\textsf{N}(#1)} %\newcommand{\norm}[1]{\textsf{Norm}(#1)} \newcommand{\semantic}[1]{{\llbracket #1 \rrbracket}} \newcommand{\tenv}[0]{\vec \alpha} \newcommand{\make@circled}[2]{% \ooalign{$\m@th#1\smallbigcirc{#1}$\cr\hidewidth$\m@th#1#2$\hidewidth\cr}% } \newcommand{\smallbigcirc}[1]{% \vcenter{\hbox{\scalebox{0.77778}{$\m@th#1\bigcirc$}}}% } \newcommand{\tsand}{\mathbin{\mathpalette\make@circled\wedge}} \newcommand{\tsor}{\mathbin{\mathpalette\make@circled\vee}} %\newcommand{\tstimes}{\otimes} \newcommand{\tstimes}{\mathbin{\mathpalette\make@circled\times}} \newcommand{\tsempty}{\Omega} \newcommand{\tsfun}[1]{{[}#1]} \newcommand{\tsfunone}[2]{{[}\arrow {#1} {#2}]} \newcommand{\ts}{\mathbbm{t}} \newcommand{\tsint}[1]{\textbf{\textup{\{}}#1\textbf{\textup{\}}}} \newcommand{\tsrep}[1]{\textsf{\textup{Repr}}(#1)} \newcommand{\vdashA}{\vdash_{\!\scriptscriptstyle\mathcal{A}}} \newcommand{\vdashAts}{\vdash_{\!\scriptscriptstyle\mathcal{A}_\text{ts}}} \newcommand{\vdashp}{\vdash^{\texttt{Path}}} \newcommand{\pvdash}[3]{\vdashp_{#1,#2,#3}}%\mathcal{P} \newcommand{\evdash}[2]{\vdash^{\texttt{Env}}_{#1,#2}} \DeclareMathSymbol{\qm}{\mathalpha}{operators}{"3F} \DeclareMathAlphabet{\mathbbm}{U}{bbold}{m}{n} \newcommand{\dyn}{\ensuremath{\mathbbm{\qm}}} \newcommand{\Aa}{\ensuremath{_{\scriptscriptstyle\mathcal{A}}}} \newcommand{\Aats}{\ensuremath{_{\scriptscriptstyle\mathcal{A}_\text{ts}}}} \newcommand{\leqA}{\leq_{\!\scriptscriptstyle\mathcal{A}}} %%%%%% Dirty hack to save some space on the first page %% \def\copyrightpermissionfootnoterule{} %% \def\maketitle{% %% \if@ACM@anonymous %% % Anonymize omission of \author-s %% \ifnum\num@authorgroups=0\author{}\fi %% \fi %% \begingroup %% \let\@footnotemark\@footnotemark@nolink %% \let\@footnotetext\@footnotetext@nolink %% \def\@makefnmark{\hbox{\@textsuperscript{\@thefnmark}}}% %% \@mktitle\if@ACM@sigchiamode\else\@mkauthors\fi\@mkteasers %% \@printtopmatter %% \if@ACM@sigchiamode\@mkauthors\fi %% \setcounter{footnote}{0}% %% \@titlenotes %% \@subtitlenotes %% \@authornotes %% \let\@makefnmark\relax %% \let\@thefnmark\relax %% \let\@makefntext\noindent %% \ifx\@empty\thankses\else %% \footnotetextauthorsaddresses{% %% \def\par{\let\par\@par}\parindent\z@\@setthanks}% %% \fi %% \ifx\@empty\@authorsaddresses\else %% \if@ACM@anonymous\else %% \if@ACM@journal %% \footnotetextauthorsaddresses{% %% \def\par{\let\par\@par}\parindent\z@\@setauthorsaddresses}% %% \fi %% \fi %% \fi %% \endgroup %% \setcounter{footnote}{0}% %% \@mkabstract %% \if@ACM@printccs %% \ifx\@concepts\@empty\else\bgroup %% {\@specialsection{CCS Concepts}% %% \@concepts\par}\egroup %% \fi %% \fi %% \andify\authors %% \andify\shortauthors %% \global\let\authors=\authors %% \global\let\shortauthors=\shortauthors %% \if@ACM@printacmref %% \@mkbibcitation %% \fi %% \hypersetup{% %% pdfauthor={\authors}, %% pdftitle={\@title}, %% pdfsubject={\@concepts}, %% pdfkeywords={\@keywords}, %% pdfcreator={LaTeX with acmart %% \csname ver@acmart.cls\endcsname\space %% and hyperref %% \csname ver@hyperref.sty\endcsname}}% %% \global\@topnum\z@ % this prevents floats from falling %% % at the top of page 1 %% \global\@botnum\z@ % we do not want them to be on the bottom either %% \@printendtopmatter %% \@afterindentfalse %% \@afterheading %% } %% \newcommand{\bbGamma}{{\mathpalette\makebbGamma\relax}} %% \newcommand{\makebbGamma}[2]{% %% \raisebox{\depth}{\scalebox{1}[-1]{$\mathsurround=0pt#1\mathbb{L}$}}% %% } %% \newcommand{\Raux}[1]{\textsf{Aux}_{#1}} %% \newcommand{\RRefine}[1]{\textsf{Refine}_{#1}} %% \newcommand{\lfp}[1]{\textsf{lfp}_{#1}} %% \newcommand{\RRefineStep}[1]{\textsf{RefineStep}_{#1}} %% \newcommand{\dt}[0]{\mathbb{T}} %% \newcommand{\fvdash}[2]{\vdash^{\texttt{Env}\rightarrow}_{#1,#2}} %% \newcommand{\bvdash}[2]{\vdash^{\texttt{Env}\leftarrow}_{#1,#2}} %% % \newcommand{\ufvdash}[3]{{\underset{#1}\vdash}^{\texttt{Env}\rightarrow}_{#2,#3}} %% % \newcommand{\ubvdash}[3]{{\underset{#1}\vdash}^{\texttt{Env}\leftarrow}_{#2,#3}} %% \newcommand{\ufvdash}[3]{\vdash^{{#1},\texttt{ Env}\rightarrow}_{#2,#3}} %% \newcommand{\ubvdash}[3]{\vdash^{{#1},\texttt{ Env}\leftarrow}_{#2,#3}} %% \newcommand{\cvdash}[0]{\vdash^{\texttt{Choices}}} %% \newcommand{\ct}[0]{\mathcal{C}} %% \newcommand{\Gammap}[0]{{\Gamma'}} %% \newcommand{\avdash}[2]{\vdash_{#1,\ #2}} %% \newcommand{\bt}[0]{\texttt{Backtrack}} %% \newcommand{\Gammas}[0]{\bbGamma} %% \newcommand{\Tree}[0]{\texttt{T}} %% \newcommand{\Node}[0]{\texttt{N}} %% \newcommand{\Leaf}[0]{\texttt{L}} %% \newcommand{\tree}[0]{\mathcal{T}} %% \newcommand{\ttype}[0]{\texttt{type}} %% \newcommand{\tleaves}[0]{\texttt{leaves}} %% \newcommand{\tnodes}[0]{\texttt{nodes}} %% \newcommand{\tlabels}[0]{\texttt{labels}} %% \newcommand{\tflatten}[0]{\texttt{flatten}} %% \newcommand{\btr}[0]{\blacktriangleright} %% \makeatletter % allow us to mention @-commands %% \def\arcr{\@arraycr} %% \makeatother