[Git][monnier/typer][report/itd] 27 commits: Switch to ACM style for ICFP - Typer

9 Mai 2020


      Stefan pushed to branch report/itd at Stefan / Typer
Commits:
bf01fe80 by Stefan Monnier at 2019-02-27T22:35:16-05:00
Switch to ACM style for ICFP
- - - - -
a07ed911 by Stefan Monnier at 2019-03-25T17:54:36-04:00
-
- - - - -
7a06cc13 by Stefan Monnier at 2019-03-27T19:59:59-04:00
Merge branch &#39;report/itd&#39; of git+ssh://iro/~/var/git/typer into report/itd
- - - - -
44dbb9fd by Stefan Monnier at 2019-03-27T23:51:10-04:00
-
- - - - -
c17ca441 by Stefan Monnier at 2019-03-28T17:56:29-04:00
-
- - - - -
eda0b211 by Stefan Monnier at 2019-05-07T22:40:31-04:00
-
- - - - -
cfb4a843 by Stefan Monnier at 2019-05-14T11:34:21-04:00
-
- - - - -
bb76755a by Stefan Monnier at 2019-05-14T18:05:11-04:00
-
- - - - -
c56cef92 by Stefan Monnier at 2019-05-15T16:55:42-04:00
-
- - - - -
df782827 by Stefan Monnier at 2019-05-17T16:22:17-04:00
-
- - - - -
47898ed6 by Stefan Monnier at 2019-05-17T23:26:10-04:00
-
- - - - -
db0f594d by Stefan Monnier at 2019-05-18T09:30:00-04:00
-
- - - - -
b9bc5b90 by Stefan Monnier at 2019-05-19T10:15:28-04:00
-
- - - - -
df512359 by Stefan Monnier at 2019-05-19T13:49:57-04:00
-
- - - - -
9e312c56 by Stefan Monnier at 2019-05-19T18:51:23-04:00
-
- - - - -
36094205 by Stefan Monnier at 2019-05-20T03:35:43-04:00
TyDe submission
- - - - -
2e8cab6c by Stefan Monnier at 2019-07-01T05:09:27-04:00
Final TyDe 2019 submission
- - - - -
f371f1cb by Stefan Monnier at 2019-07-10T17:12:36-04:00
-
- - - - -
50eee2af by Stefan Monnier at 2019-07-10T18:11:35-04:00
Final final version for TyDe
- - - - -
6568bbbc by Stefan Monnier at 2019-07-27T09:26:40-04:00
-
- - - - -
f468006e by Stefan Monnier at 2019-07-30T20:11:58-04:00
-
- - - - -
c7d59731 by Stefan Monnier at 2019-07-31T16:21:26-04:00
-
- - - - -
38bbaf4a by Stefan Monnier at 2019-07-31T18:05:16-04:00
-
- - - - -
010a4422 by Stefan Monnier at 2019-07-31T18:06:52-04:00
-
- - - - -
cee2ec13 by Stefan Monnier at 2019-08-17T04:23:56-04:00
-
- - - - -
9016ae36 by Stefan Monnier at 2019-08-17T06:54:21-04:00
-
- - - - -
e7585482 by Stefan Monnier at 2019-08-17T19:25:28-04:00
-
- - - - -
5 changed files:
- + REVIEWS
- + acmart.cls
- paper.tex
- refs.bib
- + slides.tex
Changes:
=====================================
REVIEWS
=====================================
@@ -0,0 +1,266 @@
+-*- outline -*-
+
+* Review #6A
+
+Overall merit
+-------------
+3. Weak accept
+
+Reviewer expertise
+------------------
+4. Expert
+
+Paper summary
+-------------
+This paper introduces the Calculus of United Constructions (CUC), a dependently
+typed calculus similar to the Calculus of Inductive Constructions (CIC), but
+with special attention to implementation efficiency.
+The paper first reviews several implementation inefficiencies with inductives
+types a la CIC.
+It then present CUC, feature by feature, motivating each feature with the
+implementation inefficiency it solves.
+The key idea in CUC is to encode inductive types via sums, products, and
+recursive types, and pay special attention to eliminating sums and products
+efficiently.
+Finally, the paper concludes by giving a syntactic model of CUC in CIC, and a
+partial model of CIC in CUC.
+
+Comments for author
+-------------------
+## High-level
+I liked the paper a lot.
+The usual presentation of inductive types is exceedingly and unnecessarily
+complex, and does not lend itself to optimization.
+Very little work has been presented studying simpler presentations.
+This paper does a nice job of analyzing a simpler presentation and, informally,
+its performance characterization.
+
+However, the discussion of performance is pretty informal, all at the level of
+intuition and comparison to C-like statements.
+It's not immediately clear to me that the Coq -> OCaml -> x86 compiler doesn't
+do something incredibly clever to optimize many of these cases some of the time.
+In fact, the paper points out that there are known ways to do solve some of
+these inefficiencies.
+This raises the question "if compilers are smart enough, why bother with all
+this?".
+I'd like to see some *evidence* (e.g., benchmark comparison CUC vs CIC?) that
+this calculus will pay off, but there's no hint of that in the paper.
+
+My intuition, of course, is that the compiler isn't always smart enough, so this
+is worthwhile, and I still feel pretty positive about the paper.
+
+The writing could use some work.
+The transitions are a little sudden at times.
+This makes it a little difficult to figure out the precise motivation and whether I'm completely following the author's train of thought.
+E.g.:
+- there is no abstract
+- the intro starts with Typer (a somewhat unfamiliar language; usually one moves
+  from old, familiar information to new, unfamiliar)
+- the intro jumps from the design ideas of Typer to CoC, without any transition.
+
+And there are a few imprecise or unnecessary words in various places.
+This makes it difficult to figure out what claims precisely are, and evaluate them.
+E.g.:
+- in the intro: "... single-constructor datatypes is not *really* problematic
+  in terms ...", could omit "really"
+- still in intro: "... it becomes *annoying* when extracting data out of those tuples ...",
+  what does annoying mean here?
+- bottom of page 2: "*Arguably* one could change Coq such that default
+  branches get additional ...". One could or could not change Coq; it's only
+  "arguably" a good idea.
+
+## $\Pi\Sigma$
+CUC is quite similar to the language ΠΣ by Altenkirch et al.
+While I agree with the one comment the paper makes about their work, I would
+appreciate a detailed comparison, and you have space for it.
+E.g., your `switch` statement looks pretty similar to their `case`, even in
+terms of performance (intuitively).
+
+## Projection `e.i`
+It was unclear to me until late in the paper that the projection syntax `e.i`
+was mere syntactic sugar, and not an expression missing from your presentation
+of CUC.
+I would use a different symbol than $\equiv$ to indicate that this definition is
+syntactic sugar.
+
+But actually, it seems to me that you can remove this syntax very easily, by
+writing the typing rule for tuple elimination as follows:
+
+> ...
+>
+> ————-———-———-———-———-———-——-
+>
+> $\Gamma \vdash_U
+> let,,\vec{x}\mathrel{=}e_1\mathrel{in}e\mathrel{:}let,,\vec{x}\mathrel{=}e_1\mathrel{in}\tau$
+
+It's not immediately obvious that this is well-founded, but it is since the type
+of $\tau$ cannot be dependent.
+
+## CUC to CIC
+Regarding the translation from CUC to CIC (Section 5.3), the first sentence
+needs to be rephrased.
+It reads "... translating *any* type derivation of CIC to an equivalent expression in CUC ...".
+You later point out that, actually, this doesn't always work due issues with the
+universe hierarchy, so it is not true that *any* type derivation can be translated.
+
+(Also, "translating *type derivations* into *expressions*"?)
+
+However, isn't this problem solved by adding cumulativity to CUC?
+
+
+
+* Review #6B
+===========================================================================
+
+Overall merit
+-------------
+4. Accept
+
+Reviewer expertise
+------------------
+4. Expert
+
+Paper summary
+-------------
+This paper presents the calculus of united constructions (CUC), a variant of
+the calculus of inductive constructions (CiC) where the notion of inductive
+family has been split up into labeled records, non-disjoint unions, equality
+types, and inductive fixpoints. The main objective of this calculus is to
+provide a type theory that can easily be compiled to efficient code, and can
+serve as a core language for a reflection-based surface language. The paper
+further provides two translations: a translation by erasing type annotations
+to obtain efficient code, and a translation from CiC showing conservativity
+and (relative) consistency.
+
+Comments for author
+-------------------
+I really enjoyed reading this paper since it provides careful and detailed
+motivation for all of its design decisions, and in particular pays attention
+to the often-neglected subject of efficiency and compilation of type
+theoretic languages. The primitive 'switch' operator is especially
+interesting since it allows the implementation of catchall cases without
+losing any information from the branches that were not taken, which is
+a common complaint among users of other languages. 
+
+However, the second half of the paper feels very cramped and would probably
+benefit by removing some parts to expand others. For example, the
+translation from CIC to CUC feel like it didn't add much, so it could be
+removed to make more space for the (more important) translation in the
+opposite direction. 
+
+I also felt that many claims about the supposed impact of design decisions
+on the efficiency are rather vague and are not backed by any evidence (see
+for example the remark about garbage collection at the end of section 2.1),
+so the effective impact of these decisions remains at the level of an
+educated guess.
+
+Nevertheless, I found there were a lot of new insights in this paper that
+the TyDe audience in particular would find very interesting, so I gladly
+recommend it for acceptance.
+
+Questions for the authors:
+- Some of the type annotations in the syntax (e.g. the Δ in the tuple
+constructor and the τ and p in the fold constructor) look like they are
+redundant information. Even though they are erased at runtime, they could
+still cause at typechecking time, so wouldn't it be better to remove them
+from the syntax completely?
+- The paper makes no mention of eta-equality for function or record
+types. Since this is quite an important property in practice, I was
+wondering whether this would be easy to add.
+- A potential pitfall to the language design where datatypes are encoded in
+terms of smaller components is that it makes it very hard to print good
+error messages to the user of the system. Do you know of a solution to this
+problem in the case of CUC?
+- How does CUC compare to the core language of the Lean proof assistant?
+This would be interesting since like CUC, Lean focuses on efficiency
+and reflection.
+- A technical question: the typing rule for 'let fold' (the third rule in
+Figure 7) brings the parameters of the inductive type into scope for the
+body e2, but the corresponding computation rule throws away the parameters
+(i.e. it doesn't substitute anything for the variables 'z'). How do you
+ensure that these parameters are not used?
+
+Minor remarks and typos:
+- The standard reference for Agda is Ulf Norell's thesis (Towards
+a practical programming language based on dependent types)
+- The title of section 2 is not very accurate, something like "Problem
+description" would be clearer.
+- The last paragraph of section 2.2 seems to be out of its intended context,
+I would suggest rewording it.
+- In the first sentence of section 3.2, "inductive types" should be replaced
+by "non-recursive types" since the μ type has not been introduced yet at
+this point.
+- The first typing rule in Figure 7 is confusing since it is formulated for
+an arbitrary type τ, whereas it is only used for types of the form (x1 : A1)
+... (xn : An) -> Set_l.
+- In the first sentence of section 4, "castto" should be "cast to"
+
+
+
+* Review #6C
+===========================================================================
+
+Overall merit
+-------------
+5. Strong accept
+
+Reviewer expertise
+------------------
+3. Knowledgeable
+
+Paper summary
+-------------
+The paper describes the calculus of united constructions (CUC), a new
+foundational calculus for dependently-typed programming.  CUC partitions
+datatype representations into tuples, unions, equality constraints, and
+recursive types, rather than supporting these all through a single idea of
+inductive type definition.  The resulting system, while having more forms
+than CIC, also admits more efficient implementation, and refines the typing
+of case branches.
+
+Comments for author
+-------------------
+This is an excellent paper.  I found it well-motivated and easy to read; the
+proposed formalisms are intuitive and expressive.  I strongly recommend
+its acceptance.
+
+Some detailed comments:
+
+- The typing rule for `let` in Fig. 2 seems to include some implicit
+subtyping, in the |x| < |\Delta| case.  Is this intentional, and is it
+useful?  It's not discussed in the text.
+
+- First sentence of section 4: "castto" -> "cast to"
+
+
+
+* Review #6D
+===========================================================================
+
+Overall merit
+-------------
+3. Weak accept
+
+Reviewer expertise
+------------------
+3. Knowledgeable
+
+Comments for author
+-------------------
+## Minor points
+
+- You'll need an abstract.
+
+- p2: "an value"
+
+- p2: "the fact the"
+
+- p11: "be compiling them"
+
+- p12: "Conor" has one "n"
+
+
+
+(This is not a formal review, but only comment by Jeremy Gibbons.)
+
+
=====================================
acmart.cls
=====================================
@@ -0,0 +1,2851 @@
+%%
+%% This is file `acmart.cls',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% acmart.dtx  (with options: `class')
+%% 
+%% IMPORTANT NOTICE:
+%% 
+%% For the copyright see the source file.
+%% 
+%% Any modified versions of this file must be renamed
+%% with new filenames distinct from acmart.cls.
+%% 
+%% For distribution of the original source see the terms
+%% for copying and modification in the file acmart.dtx.
+%% 
+%% This generated file may be distributed as long as the
+%% original source files, as listed above, are part of the
+%% same distribution. (The sources need not necessarily be
+%% in the same archive or directory.)
+%% \CharacterTable
+%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%%   Digits        \0\1\2\3\4\5\6\7\8\9
+%%   Exclamation   !     Double quote  "     Hash (number) #
+%%   Dollar        $     Percent       %     Ampersand     &
+%%   Acute accent  '     Left paren    (     Right paren   )
+%%   Asterisk      *     Plus          +     Comma         ,
+%%   Minus         -     Point         .     Solidus       /
+%%   Colon         :     Semicolon     ;     Less than     <
+%%   Equals        =     Greater than  >     Question mark ?
+%%   Commercial at @     Left bracket  [     Backslash     \
+%%   Right bracket ]     Circumflex    ^     Underscore    _
+%%   Grave accent  `     Left brace    {     Vertical bar  |
+%%   Right brace   }     Tilde         ~}
+\label{sec:ug_topmatter}
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesClass{acmart}
+[2019/05/27 v1.61 Typesetting articles for the Association for
+Computing Machinery]
+\def@classname{acmart}
+\InputIfFileExists{acmart-preload-hook.tex}{%
+  \ClassWarning{@classname}{%
+    I am loading acmart-preload-hook.tex. You are fully responsible
+    for any problems from now on.}}{}
+\RequirePackage{xkeyval}
+\RequirePackage{xstring}
+\define@choicekey*+{acmart.cls}{format}[\ACM@format\ACM@format@nr]{%
+  manuscript, acmsmall, acmlarge, acmtog, sigconf, siggraph,
+  sigplan, sigchi, sigchi-a}[manuscript]{}{%
+  \ClassError{@classname}{The option format must be manuscript,
+    acmsmall, acmlarge, acmtog, sigconf, siggraph,
+    sigplan, sigchi or sigchi-a}}
+\def@DeclareACMFormat#1{\DeclareOptionX{#1}{\setkeys{acmart.cls}{format=#1}}}
+@DeclareACMFormat{manuscript}
+@DeclareACMFormat{acmsmall}
+@DeclareACMFormat{acmlarge}
+@DeclareACMFormat{acmtog}
+@DeclareACMFormat{sigconf}
+@DeclareACMFormat{siggraph}
+@DeclareACMFormat{sigplan}
+@DeclareACMFormat{sigchi}
+@DeclareACMFormat{sigchi-a}
+\ExecuteOptionsX{format}
+\define@boolkey+{acmart.cls}[@ACM@]{screen}[true]{%
+  \if@ACM@screen
+    \PackageInfo{@classname}{Using screen mode}%
+  \else
+    \PackageInfo{@classname}{Not using screen mode}%
+  \fi}{\PackageError{@classname}{The option screen can be either true or
+    false}}
+\ExecuteOptionsX{screen=false}
+\define@boolkey+{acmart.cls}[@ACM@]{urlbreakonhyphens}[true]{%
+  \if@ACM@urlbreakonhyphens
+    \PackageInfo{@classname}{Using breaking urls on hyphens}%
+  \else
+    \PackageInfo{@classname}{Not breaking urls on hyphens}%
+  \fi}{\PackageError{@classname}{The option urlbreakonhyphens can be either true or
+    false}}
+\ExecuteOptionsX{urlbreakonhyphens=true}
+\define@boolkey+{acmart.cls}[@ACM@]{acmthm}[true]{%
+  \if@ACM@acmthm
+    \PackageInfo{@classname}{Requiring acmthm}%
+  \else
+    \PackageInfo{@classname}{Suppressing acmthm}%
+  \fi}{\PackageError{@classname}{The option acmthm can be either true or
+    false}}
+\ExecuteOptionsX{acmthm=true}
+\define@boolkey+{acmart.cls}[@ACM@]{review}[true]{%
+  \if@ACM@review
+    \PackageInfo{@classname}{Using review mode}%
+    \AtBeginDocument{@ACM@printfoliostrue}%
+  \else
+    \PackageInfo{@classname}{Not using review mode}%
+  \fi}{\PackageError{@classname}{The option review can be either true or
+    false}}
+\ExecuteOptionsX{review=false}
+\define@boolkey+{acmart.cls}[@ACM@]{authorversion}[true]{%
+  \if@ACM@authorversion
+    \PackageInfo{@classname}{Using authorversion mode}%
+  \else
+    \PackageInfo{@classname}{Not using authorversion mode}%
+  \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@]{balance}[true]{}{%
+  \PackageError{@classname}{The option balance can be either true or
+    false}}
+\ExecuteOptionsX{balance}
+\define@boolkey+{acmart.cls}[@ACM@]{natbib}[true]{%
+  \if@ACM@natbib
+    \PackageInfo{@classname}{Explicitly selecting natbib mode}%
+  \else
+    \PackageInfo{@classname}{Explicitly deselecting natbib mode}%
+  \fi}{\PackageError{@classname}{The option natbib can be either true or
+    false}}
+\ExecuteOptionsX{natbib=true}
+\define@boolkey+{acmart.cls}[@ACM@]{anonymous}[true]{%
+  \if@ACM@anonymous
+    \PackageInfo{@classname}{Using anonymous mode}%
+  \else
+    \PackageInfo{@classname}{Not using anonymous mode}%
+  \fi}{\PackageError{@classname}{The option anonymous can be either true or
+    false}}
+\ExecuteOptionsX{anonymous=false}
+\define@boolkey+{acmart.cls}[@ACM@]{timestamp}[true]{%
+  \if@ACM@timestamp
+    \PackageInfo{@classname}{Using timestamp mode}%
+  \else
+    \PackageInfo{@classname}{Not using timestamp mode}%
+  \fi}{\PackageError{@classname}{The option timestamp can be either true or
+    false}}
+\ExecuteOptionsX{timestamp=false}
+\define@boolkey+{acmart.cls}[@ACM@]{authordraft}[true]{%
+  \if@ACM@authordraft
+    \PackageInfo{@classname}{Using authordraft mode}%
+    @ACM@timestamptrue
+    @ACM@reviewtrue
+  \else
+    \PackageInfo{@classname}{Not using authordraft mode}%
+  \fi}{\PackageError{@classname}{The option authordraft can be either true or
+    false}}
+\ExecuteOptionsX{authordraft=false}
+\def\ACM@fontsize{}
+\DeclareOptionX{9pt}{\edef\ACM@fontsize{\CurrentOption}}
+\DeclareOptionX{10pt}{\edef\ACM@fontsize{\CurrentOption}}
+\DeclareOptionX{11pt}{\edef\ACM@fontsize{\CurrentOption}}
+\DeclareOptionX{12pt}{\edef\ACM@fontsize{\CurrentOption}}
+\DeclareOptionX{draft}{\PassOptionsToClass{\CurrentOption}{amsart}}
+\DeclareOptionX{*}{\PassOptionsToClass{\CurrentOption}{amsart}}
+\ProcessOptionsX
+\ClassInfo{@classname}{Using format \ACM@format, number \ACM@format@nr}
+\newif\if@ACM@manuscript
+\newif\if@ACM@journal
+\newif\if@ACM@journal@bibstrip
+\newif\if@ACM@sigchiamode
+\ifnum\ACM@format@nr=5\relax % siggraph
+  \ClassWarning{@classname}{The format siggraph is now obsolete.
+    I am switching to sigconf.}
+  \setkeys{acmart.cls}{format=sigconf}
+\fi
+\ifnum\ACM@format@nr=0\relax
+  @ACM@manuscripttrue
+\else
+  @ACM@manuscriptfalse
+\fi
+@ACM@sigchiamodefalse
+\ifcase\ACM@format@nr
+\relax % manuscript
+  @ACM@journaltrue
+\or % acmsmall
+  @ACM@journaltrue
+\or % acmlarge
+  @ACM@journaltrue
+\or % acmtog
+  @ACM@journaltrue
+\or % sigconf
+  @ACM@journalfalse
+\or % siggraph
+  @ACM@journalfalse
+ \or % sigplan
+  @ACM@journalfalse
+ \or % sigchi
+  @ACM@journalfalse
+\or % sigchi-a
+  @ACM@journalfalse
+  @ACM@sigchiamodetrue
+\fi
+\if@ACM@journal
+ @ACM@journal@bibstriptrue
+\else
+ @ACM@journal@bibstripfalse
+\fi
+\ifx\ACM@fontsize@empty
+  \ifcase\ACM@format@nr
+  \relax % manuscript
+    \def\ACM@fontsize{9pt}%
+  \or % acmsmall
+    \def\ACM@fontsize{10pt}%
+  \or % acmlarge
+    \def\ACM@fontsize{10pt}%
+  \or % acmtog
+    \def\ACM@fontsize{9pt}%
+  \or % sigconf
+    \def\ACM@fontsize{9pt}%
+  \or % siggraph
+    \def\ACM@fontsize{9pt}%
+   \or % sigplan
+    \def\ACM@fontsize{10pt}%
+   \or % sigchi
+    \def\ACM@fontsize{10pt}%
+  \or % sigchi-a
+    \def\ACM@fontsize{10pt}%
+  \fi
+\fi
+\ClassInfo{@classname}{Using fontsize \ACM@fontsize}
+\LoadClass[\ACM@fontsize, reqno]{amsart}
+\RequirePackage{microtype}
+\RequirePackage{etoolbox}
+\RequirePackage{booktabs}
+\RequirePackage{refcount}
+\RequirePackage{totpages}
+\RequirePackage{environ}
+\if@ACM@manuscript
+\RequirePackage{setspace}
+\onehalfspacing
+\fi
+\RequirePackage{textcase}
+\if@ACM@natbib
+  \RequirePackage{natbib}
+  \renewcommand{\bibsection}{%
+     \section*{\refname}%
+     \phantomsection\addcontentsline{toc}{section}{\refname}%
+  }
+  \renewcommand{\bibfont}{\bibliofont}
+  \renewcommand\setcitestyle[1]{
+  @for@tempa:=#1\do
+  {\def@tempb{round}\ifx@tempa@tempb
+     \renewcommand\NAT@open{(}\renewcommand\NAT@close{)}\fi
+   \def@tempb{square}\ifx@tempa@tempb
+     \renewcommand\NAT@open{[}\renewcommand\NAT@close{]}\fi
+   \def@tempb{angle}\ifx@tempa@tempb
+     \renewcommand\NAT@open{$<$}\renewcommand\NAT@close{$>$}\fi
+   \def@tempb{curly}\ifx@tempa@tempb
+     \renewcommand\NAT@open{{}\renewcommand\NAT@close{}}\fi
+   \def@tempb{semicolon}\ifx@tempa@tempb
+     \renewcommand\NAT@sep{;}\fi
+   \def@tempb{colon}\ifx@tempa@tempb
+     \renewcommand\NAT@sep{;}\fi
+   \def@tempb{comma}\ifx@tempa@tempb
+     \renewcommand\NAT@sep{,}\fi
+   \def@tempb{authoryear}\ifx@tempa@tempb
+     \NAT@numbersfalse\fi
+   \def@tempb{numbers}\ifx@tempa@tempb
+     \NAT@numberstrue\NAT@superfalse\fi
+   \def@tempb{super}\ifx@tempa@tempb
+     \NAT@numberstrue\NAT@supertrue\fi
+   \def@tempb{nobibstyle}\ifx@tempa@tempb
+     \let\bibstyle=@gobble\fi
+   \def@tempb{bibstyle}\ifx@tempa@tempb
+     \let\bibstyle=@citestyle\fi
+   \def@tempb{sort}\ifx@tempa@tempb
+     \def\NAT@sort{@ne}\fi
+   \def@tempb{nosort}\ifx@tempa@tempb
+     \def\NAT@sort{\z@}\fi
+   \def@tempb{compress}\ifx@tempa@tempb
+     \def\NAT@cmprs{@ne}\fi
+   \def@tempb{nocompress}\ifx@tempa@tempb
+     \def\NAT@cmprs{\z@}\fi
+   \def@tempb{sort&compress}\ifx@tempa@tempb
+     \def\NAT@sort{@ne}\def\NAT@cmprs{@ne}\fi
+   \def@tempb{mcite}\ifx@tempa@tempb
+     \let\NAT@merge@ne\fi
+   \def@tempb{merge}\ifx@tempa@tempb
+     @ifnum{\NAT@merge<\tw@}{\let\NAT@merge\tw@}{}\fi
+   \def@tempb{elide}\ifx@tempa@tempb
+     @ifnum{\NAT@merge<\thr@@}{\let\NAT@merge\thr@@}{}\fi
+   \def@tempb{longnamesfirst}\ifx@tempa@tempb
+     \NAT@longnamestrue\fi
+   \def@tempb{nonamebreak}\ifx@tempa@tempb
+     \def\NAT@nmfmt#1{\mbox{\NAT@up#1}}\fi
+   \expandafter\NAT@find@eq@tempa=\relax@nil
+   \if@tempc\relax\else
+     \expandafter\NAT@rem@eq@tempc
+     \def@tempb{open}\ifx@tempa@tempb
+      \xdef\NAT@open{@tempc}\fi
+     \def@tempb{close}\ifx@tempa@tempb
+      \xdef\NAT@close{@tempc}\fi
+     \def@tempb{aysep}\ifx@tempa@tempb
+      \xdef\NAT@aysep{@tempc}\fi
+     \def@tempb{yysep}\ifx@tempa@tempb
+      \xdef\NAT@yrsep{@tempc}\fi
+     \def@tempb{notesep}\ifx@tempa@tempb
+      \xdef\NAT@cmt{@tempc}\fi
+     \def@tempb{citesep}\ifx@tempa@tempb
+      \xdef\NAT@sep{@tempc}\fi
+   \fi
+  }%
+  \NAT@@setcites
+  }
+  \renewcommand\citestyle[1]{%
+    \ifcsname bibstyle@#1\endcsname%
+    \csname bibstyle@#1\endcsname\let\bibstyle@gobble%
+    \else%
+    @latex@error{Undefined `#1' citestyle}%
+    \fi
+  }%
+\fi
+\newcommand{\bibstyle@acmauthoryear}{%
+  \setcitestyle{%
+    authoryear,%
+    open={[},close={]},citesep={;},%
+    aysep={},yysep={,},%
+    notesep={, }}}
+\newcommand{\bibstyle@acmnumeric}{%
+  \setcitestyle{%
+    numbers,sort&compress,%
+    open={[},close={]},citesep={,},%
+    notesep={, }}}
+\if@ACM@natbib
+\citestyle{acmnumeric}
+\fi
+\def@startsection#1#2#3#4#5#6{%
+  \if@noskipsec \leavevmode \fi
+  \par
+  @tempskipa #4\relax
+  @afterindenttrue
+  \ifdim @tempskipa <\z@
+    @tempskipa -@tempskipa @afterindentfalse
+  \fi
+  \if@nobreak
+    \everypar{}%
+  \else
+    \addpenalty@secpenalty\addvspace@tempskipa
+  \fi
+  @ifstar
+    {@ssect{#3}{#4}{#5}{#6}}%
+    {@dblarg{@sect{#1}{#2}{#3}{#4}{#5}{#6}}}}
+\def@sect#1#2#3#4#5#6[#7]#8{%
+  \edef@toclevel{\ifnum#2=@m 0\else\number#2\fi}%
+  \ifnum #2>\c@secnumdepth
+    \let@svsec@empty
+  \else
+    \refstepcounter{#1}%
+    \protected@edef@svsec{@seccntformat{#1}\relax}%
+  \fi
+  @tempskipa #5\relax
+  \ifdim @tempskipa>\z@
+    \begingroup
+      #6{%
+        @hangfrom{\hskip #3\relax@svsec}%
+          \interlinepenalty @M #8@@par}%
+    \endgroup
+    \csname #1mark\endcsname{#7}%
+    \ifnum #2>\c@secnumdepth \else
+        @tochangmeasure{\csname the#1\endcsname}%
+    \fi
+    \addcontentsline{toc}{#1}{%
+      \ifnum #2>\c@secnumdepth \else
+        \protect\numberline{\csname the#1\endcsname}%
+      \fi
+      #7}%
+  \else
+    \def@svsechd{%
+      #6{\hskip #3\relax
+      @svsec #8}%
+      \csname #1mark\endcsname{#7}%
+      \ifnum #2>\c@secnumdepth \else
+        @tochangmeasure{\csname the#1\endcsname\space}%
+      \fi
+      \addcontentsline{toc}{#1}{%
+        \ifnum #2>\c@secnumdepth \else
+          \protect\numberline{\csname the#1\endcsname}%
+        \fi
+        #7}}%
+  \fi
+  @xsect{#5}}
+\def@xsect#1{%
+  @tempskipa #1\relax
+  \ifdim @tempskipa>\z@
+    \par \nobreak
+    \vskip @tempskipa
+    @afterheading
+  \else
+    @nobreakfalse
+    \global@noskipsectrue
+    \everypar{%
+      \if@noskipsec
+        \global@noskipsecfalse
+       {\setbox\z@\lastbox}%
+        \clubpenalty@M
+        \begingroup @svsechd \endgroup
+        \unskip
+        @tempskipa #1\relax
+        \hskip -@tempskipa
+      \else
+        \clubpenalty @clubpenalty
+        \everypar{}%
+      \fi}%
+  \fi
+  \ignorespaces}
+\def@seccntformat#1{\csname the#1\endcsname\quad}
+\def@ssect#1#2#3#4#5{%
+  @tempskipa #3\relax
+  \ifdim @tempskipa>\z@
+    \begingroup
+      #4{%
+        @hangfrom{\hskip #1}%
+          \interlinepenalty @M #5@@par}%
+    \endgroup
+  \else
+    \def@svsechd{#4{\hskip #1\relax #5}}%
+  \fi
+  @xsect{#3}}
+\def@starttoc#1#2{\begingroup\makeatletter
+  \setTrue{#1}%
+  \par\removelastskip\vskip\z@skip
+  @startsection{section}@M\z@{\linespacing@plus\linespacing}%
+    {.5\linespacing}{\centering\contentsnamefont}{#2}%
+  @input{\jobname.#1}%
+  \if@filesw
+    @xp\newwrite\csname tf@#1\endcsname
+    \immediate@xp\openout\csname tf@#1\endcsname \jobname.#1\relax
+  \fi
+  \global@nobreakfalse \endgroup
+  \addvspace{32\p@@plus14\p@}%
+}
+\def\l@section{@tocline{1}{0pt}{1pc}{2pc}{}}
+\def\l@subsection{@tocline{2}{0pt}{1pc}{3pc}{}}
+\def\l@subsubsection{@tocline{2}{0pt}{1pc}{5pc}{}}
+\def@makefntext{\noindent@makefnmark}
+\if@ACM@sigchiamode
+\long\def@footnotetext#1{\marginpar{%
+    \reset@font\small
+    \interlinepenalty\interfootnotelinepenalty
+    \protected@edef@currentlabel{%
+       \csname p@footnote\endcsname@thefnmark
+    }%
+    \color@begingroup
+      @makefntext{%
+        \rule\z@\footnotesep\ignorespaces#1@finalstrut\strutbox}%
+    \color@endgroup}}%
+\fi
+\long\def@mpfootnotetext#1{%
+  \global\setbox@mpfootins\vbox{%
+    \unvbox@mpfootins
+    \reset@font\footnotesize
+    \hsize\columnwidth
+    @parboxrestore
+    \protected@edef@currentlabel
+         {\csname p@mpfootnote\endcsname@thefnmark}%
+    \color@begingroup\centering
+      @makefntext{%
+        \rule\z@\footnotesep\ignorespaces#1@finalstrut\strutbox}%
+    \color@endgroup}}
+\def@makefnmark{\hbox{@textsuperscript{\normalfont@thefnmark}}}
+\let@footnotemark@nolink@footnotemark
+\let@footnotetext@nolink@footnotetext
+\RequirePackage[bookmarksnumbered,unicode]{hyperref}
+\pdfstringdefDisableCommands{%
+  \def\addtocounter#1#2{}%
+  \def\unskip{}%
+  \def\textbullet{- }%
+  \def\textrightarrow{ -> }%
+  \def\footnotemark{}%
+}
+\urlstyle{rm}
+\ifcase\ACM@format@nr
+\relax % manuscript
+\or % acmsmall
+\or % acmlarge
+\or % acmtog
+\or % sigconf
+\or % siggraph
+\or % sigplan
+  \urlstyle{sf}
+\or % sigchi
+\or % sigchi-a
+  \urlstyle{sf}
+\fi
+\AtEndPreamble{%
+  \if@ACM@urlbreakonhyphens
+    \def\do@url@hyp{\do-}%
+  \fi
+  \if@ACM@screen
+    \hypersetup{colorlinks,
+      linkcolor=ACMPurple,
+      citecolor=ACMPurple,
+      urlcolor=ACMDarkBlue,
+      filecolor=ACMDarkBlue}
+    \else
+    \hypersetup{hidelinks}
+  \fi
+  \hypersetup{pdflang={en},
+    pdfdisplaydoctitle}}
+\if@ACM@natbib
+  \let\citeN\cite
+  \let\cite\citep
+  \let\citeANP\citeauthor
+  \let\citeNN\citeyearpar
+  \let\citeyearNP\citeyear
+  \let\citeNP\citealt
+  \DeclareRobustCommand\citeA
+     {\begingroup\NAT@swafalse
+       \let\NAT@ctype@ne\NAT@partrue\NAT@fullfalse\NAT@open\NAT@citetp}%
+  \providecommand\newblock{}%
+\else
+  \AtBeginDocument{%
+    \let\shortcite\cite%
+    \providecommand\citename[1]{#1}}
+\fi
+\newcommand\shortcite[2][]{%
+  \ifNAT@numbers\cite[#1]{#2}\else\citeyearpar[#1]{#2}\fi}
+\def\bibliographystyle#1{%
+  \ifx@begindocumenthook@undefined\else
+    \expandafter\AtBeginDocument
+  \fi
+    {\if@filesw
+       \immediate\write@auxout{\string\bibstyle{#1}}%
+     \fi}}
+\RequirePackage{graphicx}
+\RequirePackage[prologue]{xcolor}
+\definecolor[named]{ACMBlue}{cmyk}{1,0.1,0,0.1}
+\definecolor[named]{ACMYellow}{cmyk}{0,0.16,1,0}
+\definecolor[named]{ACMOrange}{cmyk}{0,0.42,1,0.01}
+\definecolor[named]{ACMRed}{cmyk}{0,0.90,0.86,0}
+\definecolor[named]{ACMLightBlue}{cmyk}{0.49,0.01,0,0}
+\definecolor[named]{ACMGreen}{cmyk}{0.20,0,1,0.19}
+\definecolor[named]{ACMPurple}{cmyk}{0.55,1,0,0.15}
+\definecolor[named]{ACMDarkBlue}{cmyk}{1,0.58,0,0.21}
+\if@ACM@authordraft
+  \RequirePackage{draftwatermark}
+  \SetWatermarkFontSize{0.5in}
+  \SetWatermarkColor[gray]{.9}
+  \SetWatermarkText{\parbox{12em}{\centering
+      Unpublished working draft.\
+      Not for distribution.}}
+\fi
+\RequirePackage{geometry}
+\ifcase\ACM@format@nr
+\relax % manuscript
+   \geometry{letterpaper,head=13pt,
+   marginparwidth=6pc,heightrounded}%
+\or % acmsmall
+   \geometry{twoside=true,
+     includeheadfoot, head=13pt, foot=2pc,
+     paperwidth=6.75in, paperheight=10in,
+     top=58pt, bottom=44pt, inner=46pt, outer=46pt,
+     marginparwidth=2pc,heightrounded
+   }%
+\or % acmlarge
+   \geometry{twoside=true, head=13pt, foot=2pc,
+     paperwidth=8.5in, paperheight=11in,
+     includeheadfoot,
+     top=78pt, bottom=114pt, inner=81pt, outer=81pt,
+     marginparwidth=4pc,heightrounded
+     }%
+\or % acmtog
+   \geometry{twoside=true, head=13pt, foot=2pc,
+     paperwidth=8.5in, paperheight=11in,
+     includeheadfoot, columnsep=24pt,
+     top=52pt, bottom=75pt, inner=52pt, outer=52pt,
+     marginparwidth=2pc,heightrounded
+     }%
+\or % sigconf
+   \geometry{twoside=true, head=13pt,
+     paperwidth=8.5in, paperheight=11in,
+     includeheadfoot, columnsep=2pc,
+     top=57pt, bottom=73pt, inner=54pt, outer=54pt,
+     marginparwidth=2pc,heightrounded
+     }%
+\or % siggraph
+   \geometry{twoside=true, head=13pt,
+     paperwidth=8.5in, paperheight=11in,
+     includeheadfoot, columnsep=2pc,
+     top=57pt, bottom=73pt, inner=54pt, outer=54pt,
+     marginparwidth=2pc,heightrounded
+     }%
+\or % sigplan
+   \geometry{twoside=true, head=13pt,
+     paperwidth=8.5in, paperheight=11in,
+     includeheadfoot=false, columnsep=2pc,
+     top=1in, bottom=1in, inner=0.75in, outer=0.75in,
+     marginparwidth=2pc,heightrounded
+     }%
+\or % sigchi
+   \geometry{twoside=true, head=13pt,
+     paperwidth=8.5in, paperheight=11in,
+     includeheadfoot, columnsep=2pc,
+     top=66pt, bottom=73pt, inner=54pt, outer=54pt,
+     marginparwidth=2pc,heightrounded
+     }%
+\or % sigchi-a
+   \geometry{twoside=false, head=13pt,
+     paperwidth=11in, paperheight=8.5in,
+     includeheadfoot, marginparsep=72pt,
+     marginparwidth=170pt, columnsep=20pt,
+     top=72pt, bottom=72pt, left=314pt, right=72pt
+     }%
+     @mparswitchfalse
+     \reversemarginpar
+\fi
+\setlength\parindent{10\p@}
+\setlength\parskip{\z@}
+\ifcase\ACM@format@nr
+\relax % manuscript
+\or % acmsmall
+\or % acmlarge
+\or % acmtog
+  \setlength\parindent{9\p@}%
+\or % sigconf
+\or % siggraph
+\or % sigplan
+\or % sigchi
+\or % sigchi-a
+\fi
+\setlength\normalparindent{\parindent}
+\def\copyrightpermissionfootnoterule{\kern-3\p@
+  \hrule @width \columnwidth \kern 2.6\p@}
+\RequirePackage{manyfoot}
+\SelectFootnoteRule[2]{copyrightpermission}
+\DeclareNewFootnote{authorsaddresses}
+\SelectFootnoteRule[2]{copyrightpermission}
+\DeclareNewFootnote{copyrightpermission}
+\def\footnoterule{\kern-3\p@
+  \hrule @width 4pc \kern 2.6\p@}
+\def\endminipage{%
+    \par
+    \unskip
+    \ifvoid@mpfootins\else
+      \vskip\skip@mpfootins
+      \normalcolor
+      \unvbox@mpfootins
+    \fi
+    @minipagefalse
+  \color@endgroup
+  \egroup
+  \expandafter@iiiparbox@mpargs{\unvbox@tempboxa}}
+\def@textbottom{\vskip \z@ @plus 1pt}
+\let@texttop\relax
+\ifcase\ACM@format@nr
+\relax % manuscript
+\or % acmsmall
+\or % acmlarge
+\or % acmtog
+  \flushbottom
+\or % sigconf
+  \flushbottom
+\or % siggraph
+  \flushbottom
+\or % sigplan
+  \flushbottom
+\or % sigchi
+  \flushbottom
+\or % sigchi-a
+\fi
+\RequirePackage{iftex}
+\ifPDFTeX
+\input{glyphtounicode}
+\pdfglyphtounicode{f_f}{FB00}
+\pdfglyphtounicode{f_f_i}{FB03}
+\pdfglyphtounicode{f_f_l}{FB04}
+\pdfglyphtounicode{f_i}{FB01}
+\pdfglyphtounicode{t_t}{0074 0074}
+\pdfglyphtounicode{f_t}{0066 0074}
+\pdfglyphtounicode{T_h}{0054 0068}
+\pdfgentounicode=1
+\fi
+\RequirePackage{cmap}
+\newif\if@ACM@newfonts
+@ACM@newfontstrue
+\IfFileExists{libertine.sty}{}{\ClassWarning{@classname}{You do not
+    have the libertine package installed.  Please upgrade your
+    TeX}@ACM@newfontsfalse}
+\IfFileExists{zi4.sty}{}{\ClassWarning{@classname}{You do not
+    have the zi4 package installed.  Please upgrade your
+    TeX}@ACM@newfontsfalse}
+\IfFileExists{newtxmath.sty}{}{\ClassWarning{@classname}{You do not
+    have the newtxmath package installed.  Please upgrade your
+    TeX}@ACM@newfontsfalse}
+\if@ACM@newfonts
+  \RequirePackage[T1]{fontenc}
+\ifxetex
+  \RequirePackage[tt=false]{libertine}
+  \setmonofont{inconsolata}
+\else
+  \RequirePackage[tt=false, type1=true]{libertine}
+\fi
+\RequirePackage[varqu]{zi4}
+\RequirePackage[libertine]{newtxmath}
+\fi
+\let\liningnums@undefined
+\AtEndPreamble{%
+  \DeclareTextFontCommand{\liningnums}{\libertineLF}}
+\if@ACM@sigchiamode
+  \renewcommand{\familydefault}{\sfdefault}
+\fi
+\newif\if@Description@present
+@Description@presenttrue
+\newif\if@undescribed@images
+@undescribed@imagesfalse
+\newcommand\Description[2][]{\global@Description@presenttrue\ignorespaces}
+\AtEndDocument{\if@undescribed@images
+  \ClassWarningNoLine{@classname}{Some images may lack descriptions}\fi}
+\AtBeginEnvironment{figure}{@Description@presentfalse
+  \let@vspace@vspace@orig
+  \let@vspacer@vspacer@orig}
+\AtBeginEnvironment{figure*}{@Description@presentfalse
+  \let@vspace@vspace@orig
+  \let@vspacer@vspacer@orig}
+\AtEndEnvironment{figure}{\if@Description@present\else
+  \global@undescribed@imagestrue
+  \ClassWarning{@classname}{A possible image without description}\fi}
+\AtEndEnvironment{figure*}{\if@Description@present\else
+  \global@undescribed@imagestrue
+  \ClassWarning{@classname}{A possible image without description}\fi}
+\AtBeginEnvironment{table}{\let@vspace@vspace@orig
+  \let@vspacer@vspacer@orig}
+\AtBeginEnvironment{table*}{\let@vspace@vspace@orig
+  \let@vspacer@vspacer@orig}
+\RequirePackage{caption, float}
+\captionsetup[table]{position=top}
+\if@ACM@journal
+  \captionsetup{labelfont={sf, small},
+    textfont={sf, small}, margin=\z@}
+  \captionsetup[figure]{name={Fig.}}
+\else
+  \captionsetup{labelfont={bf},
+    textfont={bf}, labelsep=colon, margin=\z@}
+  \ifcase\ACM@format@nr
+  \relax % manuscript
+  \or % acmsmall
+  \or % acmlarge
+  \or % acmtog
+  \or % sigconf
+  \or % siggraph
+    \captionsetup{textfont={it}}
+  \or % sigplan
+    \captionsetup{labelfont={bf},
+      textfont={normalfont}, labelsep=period, margin=\z@}
+  \or % sigchi
+    \captionsetup[figure]{labelfont={bf, small},
+      textfont={bf, small}}
+    \captionsetup[table]{labelfont={bf, small},
+      textfont={bf, small}}
+  \or % sigchi-a
+    \captionsetup[figure]{labelfont={bf, small},
+      textfont={bf, small}}
+    \captionsetup[table]{labelfont={bf, small},
+      textfont={bf, small}}
+  \fi
+\fi
+\newfloat{sidebar}{}{sbar}
+\floatname{sidebar}{Sidebar}
+\renewenvironment{sidebar}{\Collect@Body@sidebar}{}
+\long\def@sidebar#1{\bgroup\let@vspace@vspace@orig
+  \let@vspacer@vspacer@orig\captionsetup{type=sidebar}%
+  \marginpar{\small#1}\egroup}
+\newenvironment{marginfigure}{\Collect@Body@marginfigure}{}
+\long\def@marginfigure#1{\bgroup
+  \let@vspace@vspace@orig
+  \let@vspacer@vspacer@orig
+  \captionsetup{type=figure}%
+  \marginpar{@Description@presentfalse\centering
+    \small#1\if@Description@present\else
+      \global@undescribed@imagestrue
+      \ClassWarning{@classname}{A possible image without description}
+      \fi}%
+  \egroup}
+\newenvironment{margintable}{\Collect@Body@margintable}{}
+\long\def@margintable#1{\bgroup\let@vspace@vspace@orig
+  \let@vspacer@vspacer@orig\captionsetup{type=table}%
+  \marginpar{\centering\small#1}\egroup}
+\newdimen\fulltextwidth
+\fulltextwidth=\dimexpr(\textwidth+\marginparwidth+\marginparsep)
+\if@ACM@sigchiamode
+\def@dblfloat{\bgroup\let@vspace@vspace@orig
+  \let@vspacer@vspacer@orig\columnwidth=\fulltextwidth
+  \let@endfloatbox@endwidefloatbox
+  \def@fpsadddefault{\def@fps{tp}}%
+  @float}
+\fi
+\if@ACM@sigchiamode
+\def\end@dblfloat{%
+    \end@float\egroup}
+\fi
+\def@endwidefloatbox{%
+  \par\vskip\z@skip
+  @minipagefalse
+  \outer@nobreak
+  \egroup
+  \color@endbox
+  \global\setbox@currbox=\vbox{\moveleft
+    \dimexpr(\fulltextwidth-\textwidth)\box@currbox}%
+  \wd@currbox=\textwidth
+}
+\ifcase\ACM@format@nr
+\relax % manuscript
+\or % acmsmall
+\or % acmlarge
+\or % acmtog
+\or % sigconf
+\or % siggraph
+\or % sigplan
+\def\labelenumi{\theenumi.}
+\def\labelenumii{\theenumii.}
+\def\labelenumiii{\theenumiii.}
+\def\labelenumiv{\theenumiv.}
+\or % sigchi
+\or % sigchi-a
+\fi
+\newdimen@ACM@labelwidth
+\AtBeginDocument{%
+  \setlength\labelsep{4pt}
+  \setlength{@ACM@labelwidth}{6.5pt}
+
+  %% First-level list: when beginning after the first line of an
+  %% indented paragraph or ending before an indented paragraph, labels
+  %% should not hang to the left of the preceding/following text.
+  \setlength\leftmargini{\z@}
+  \addtolength\leftmargini{\parindent}
+  \addtolength\leftmargini{2\labelsep}
+  \addtolength\leftmargini{@ACM@labelwidth}
+
+  %% Second-level and higher lists.
+  \setlength\leftmarginii{\z@}
+  \addtolength\leftmarginii{0.5\labelsep}
+  \addtolength\leftmarginii{@ACM@labelwidth}
+  \setlength\leftmarginiii{\leftmarginii}
+  \setlength\leftmarginiv{\leftmarginiii}
+  \setlength\leftmarginv{\leftmarginiv}
+  \setlength\leftmarginvi{\leftmarginv}
+  @listi}
+\newskip\listisep
+\listisep\smallskipamount
+\def@listI{\leftmargin\leftmargini
+  \labelwidth\leftmargini \advance\labelwidth-\labelsep
+  \listparindent\z@
+  \topsep\listisep}
+\let@listi@listI
+\def@listii{\leftmargin\leftmarginii
+  \labelwidth\leftmarginii \advance\labelwidth-\labelsep
+  \topsep\z@skip}
+\def@listiii{\leftmargin\leftmarginiii
+  \labelwidth\leftmarginiii \advance\labelwidth-\labelsep}
+\def@listiv{\leftmargin\leftmarginiv
+  \labelwidth\leftmarginiv \advance\labelwidth-\labelsep}
+\def@listv{\leftmargin\leftmarginv
+  \labelwidth\leftmarginv \advance\labelwidth-\labelsep}
+\def@listvi{\leftmargin\leftmarginvi
+  \labelwidth\leftmarginvi \advance\labelwidth-\labelsep}
+\renewcommand{\descriptionlabel}[1]{\upshape\bfseries #1}
+\renewenvironment{description}{\list{}{%
+    \labelwidth@ACM@labelwidth
+    \let\makelabel\descriptionlabel}%
+}{
+  \endlist
+}
+\let\enddescription=\endlist % for efficiency
+\define@choicekey*+{ACM}{acmJournal}[@journalCode@journalCode@nr]{%
+  CIE,%
+  CSUR,%
+  DTRAP,%
+  HEALTH,%
+  IMWUT,%
+  JACM,%
+  JDIQ,%
+  JEA,%
+  JERIC,%
+  JETC,%
+  JOCCH,%
+  PACMCGIT,%
+  PACMHCI,%
+  PACMPL,%
+  POMACS,%
+  TAAS,%
+  TACCESS,%
+  TACO,%
+  TALG,%
+  TALLIP,%
+  TAP,%
+  TCPS,%
+  TDS,%
+  TEAC,%
+  TECS,%
+  THRI,%
+  TIIS,%
+  TIOT,%
+  TISSEC,%
+  TIST,%
+  TKDD,%
+  TMIS,%
+  TOCE,%
+  TOCHI,%
+  TOCL,%
+  TOCS,%
+  TOCT,%
+  TODAES,%
+  TODS,%
+  TOG,%
+  TOIS,%
+  TOIT,%
+  TOMACS,%
+  TOMM,%
+  TOMPECS,%
+  TOMS,%
+  TOPC,%
+  TOPS,%
+  TOPLAS,%
+  TOS,%
+  TOSEM,%
+  TOSN,%
+  TRETS,%
+  TSAS,%
+  TSC,%
+  TSLP,%
+  TWEB%
+}{%
+\ifcase@journalCode@nr
+\relax % CIE
+  \def@journalName{ACM Computers in Entertainment}%
+  \def@journalNameShort{ACM Comput. Entertain.}%
+  \def@permissionCodeOne{1544-3574}%
+\or % CSUR
+  \def@journalName{ACM Computing Surveys}%
+  \def@journalNameShort{ACM Comput. Surv.}%
+  \def@permissionCodeOne{0360-0300}%
+\or % DTRAP
+  \def@journalName{Digital Threats: Research and Practice}%
+  \def@journalNameShort{Digit. Threat. Res. Pract.}%
+  \def@permissionCodeOne{2576-5337}%
+\or % HEALTH
+  \def@journalName{ACM Transactions on Computing for Healthcare}%
+  \def@journalNameShort{ACM Trans. Comput. Healthcare}%
+  \def@permissionCodeOne{2637-8051}%
+\or % IMWUT
+  \def@journalName{Proceedings of the ACM on Interactive, Mobile,
+    Wearable and Ubiquitous Technologies}%
+  \def@journalNameShort{Proc. ACM Interact. Mob. Wearable Ubiquitous Technol.}%
+  \def@permissionCodeOne{2474-9567}%
+  @ACM@screentrue
+  \PackageInfo{@classname}{Using screen mode due to @journalCode}%
+\or % JACM
+  \def@journalName{Journal of the ACM}%
+  \def@journalNameShort{J. ACM}%
+  \def@permissionCodeOne{0004-5411}%
+\or % JDIQ
+  \def@journalName{ACM Journal of Data and Information Quality}%
+  \def@journalNameShort{ACM J. Data Inform. Quality}%
+  \def@permissionCodeOne{1936-1955}%
+\or % JEA
+  \def@journalName{ACM Journal of Experimental Algorithmics}%
+  \def@journalNameShort{ACM J. Exp. Algor.}%
+  \def@permissionCodeOne{1084-6654}%
+\or % JERIC
+  \def@journalName{ACM Journal of Educational Resources in Computing}%
+  \def@journalNameShort{ACM J. Edu. Resources in Comput.}%
+  \def@permissionCodeOne{1073-0516}%
+\or % JETC
+  \def@journalName{ACM Journal on Emerging Technologies in Computing Systems}%
+  \def@journalNameShort{ACM J. Emerg. Technol. Comput. Syst.}%
+  \def@permissionCodeOne{1550-4832}%
+\or % JOCCH
+  \def@journalName{ACM Journal on Computing and Cultural Heritage}%
+  \def@journalNameShort{ACM J. Comput. Cult. Herit.}%
+\or % PACMCGIT
+  \def@journalName{Proceedings of the ACM on Computer Graphics and Interactive Techniques}%
+  \def@journalNameShort{Proc. ACM Comput. Graph. Interact. Tech.}%
+  \def@permissionCodeOne{2577-6193}%
+  @ACM@screentrue
+  \PackageInfo{@classname}{Using screen mode due to @journalCode}%
+\or % PACMHCI
+  \def@journalName{Proceedings of the ACM on Human-Computer Interaction}%
+  \def@journalNameShort{Proc. ACM Hum.-Comput. Interact.}%
+  \def@permissionCodeOne{2573-0142}%
+  @ACM@screentrue
+  \PackageInfo{@classname}{Using screen mode due to @journalCode}%
+\or % PACMPL
+  \def@journalName{Proceedings of the ACM on Programming Languages}%
+  \def@journalNameShort{Proc. ACM Program. Lang.}%
+  \def@permissionCodeOne{2475-1421}%
+  @ACM@screentrue
+  \PackageInfo{@classname}{Using screen mode due to @journalCode}%
+\or % POMACS
+  \def@journalName{Proceedings of the ACM on Measurement and Analysis of Computing Systems}%
+  \def@journalNameShort{Proc. ACM Meas. Anal. Comput. Syst.}%
+  \def@permissionCodeOne{2476-1249}%
+  @ACM@screentrue
+  \PackageInfo{@classname}{Using screen mode due to @journalCode}%
+\or % TAAS
+  \def@journalName{ACM Transactions on Autonomous and Adaptive Systems}%
+  \def@journalNameShort{ACM Trans. Autonom. Adapt. Syst.}%
+  \def@permissionCodeOne{1556-4665}%
+\or % TACCESS
+  \def@journalName{ACM Transactions on Accessible Computing}%
+  \def@journalNameShort{ACM Trans. Access. Comput.}%
+  \def@permissionCodeOne{1936-7228}%
+\or % TACO
+  \def@journalName{ACM Transactions on Architecture and Code Optimization}%
+  \def@journalNameShort{ACM Trans. Arch. Code Optim.}%
+\or % TALG
+  \def@journalName{ACM Transactions on Algorithms}%
+  \def@journalNameShort{ACM Trans. Algor.}%
+  \def@permissionCodeOne{1549-6325}%
+\or % TALLIP
+  \def@journalName{ACM Transactions on Asian and Low-Resource Language Information Processing}%
+  \def@journalNameShort{ACM Trans. Asian Low-Resour. Lang. Inf. Process.}%
+  \def@permissionCodeOne{2375-4699}%
+\or % TAP
+  \def@journalName{ACM Transactions on Applied Perception}%
+\or % TCPS
+  \def@journalName{ACM Transactions on Cyber-Physical Systems}%
+\or % TDS
+  \def@journalName{ACM Transactions on Data Science}%
+  \def@journalNameShort{ACM Trans. Data Sci.}%
+  \def@permissionCodeOne{2577-3224}%
+\or % TEAC
+  \def@journalName{ACM Transactions on Economics and Computation}%
+\or % TECS
+  \def@journalName{ACM Transactions on Embedded Computing Systems}%
+  \def@journalNameShort{ACM Trans. Embedd. Comput. Syst.}%
+  \def@permissionCodeOne{1539-9087}%
+\or % THRI
+  \def@journalName{ACM Transactions on Human-Robot Interaction}%
+  \def@journalNameShort{ACM Trans. Hum.-Robot Interact.}%
+  \def@permissionCodeOne{2573-9522}%
+\or % TIIS
+  \def@journalName{ACM Transactions on Interactive Intelligent Systems}%
+  \def@journalNameShort{ACM Trans. Interact. Intell. Syst.}%
+  \def@permissionCodeOne{2160-6455}%
+\or % TIOT
+  \def@journalName{ACM Transactions on Internet of Things}%
+  \def@journalNameShort{ACM Trans. Internet Things}%
+  \def@permissionCodeOne{2577-6207}%
+\or % TISSEC
+  \def@journalName{ACM Transactions on Information and System Security}%
+  \def@journalNameShort{ACM Trans. Info. Syst. Sec.}%
+  \def@permissionCodeOne{1094-9224}%
+\or % TIST
+  \def@journalName{ACM Transactions on Intelligent Systems and Technology}%
+  \def@journalNameShort{ACM Trans. Intell. Syst. Technol.}%
+  \def@permissionCodeOne{2157-6904}%
+\or % TKDD
+  \def@journalName{ACM Transactions on Knowledge Discovery from Data}%
+  \def@journalNameShort{ACM Trans. Knowl. Discov. Data.}%
+  \def@permissionCodeOne{1556-4681}%
+\or % TMIS
+  \def@journalName{ACM Transactions on Management Information Systems}%
+  \def@journalNameShort{ACM Trans. Manag. Inform. Syst.}%
+  \def@permissionCodeOne{2158-656X}%
+\or % TOCE
+  \def@journalName{ACM Transactions on Computing Education}%
+  \def@journalNameShort{ACM Trans. Comput. Educ.}%
+  \def@permissionCodeOne{1946-6226}%
+\or % TOCHI
+  \def@journalName{ACM Transactions on Computer-Human Interaction}%
+  \def@journalNameShort{ACM Trans. Comput.-Hum. Interact.}%
+  \def@permissionCodeOne{1073-0516}%
+\or % TOCL
+  \def@journalName{ACM Transactions on Computational Logic}%
+  \def@journalNameShort{ACM Trans. Comput. Logic}%
+  \def@permissionCodeOne{1529-3785}%
+\or % TOCS
+  \def@journalName{ACM Transactions on Computer Systems}%
+  \def@journalNameShort{ACM Trans. Comput. Syst.}%
+  \def@permissionCodeOne{0734-2071}%
+\or % TOCT
+  \def@journalName{ACM Transactions on Computation Theory}%
+  \def@journalNameShort{ACM Trans. Comput. Theory}%
+  \def@permissionCodeOne{1942-3454}%
+\or % TODAES
+  \def@journalName{ACM Transactions on Design Automation of Electronic Systems}%
+  \def@journalNameShort{ACM Trans. Des. Autom. Electron. Syst.}%
+  \def@permissionCodeOne{1084-4309}%
+\or % TODS
+  \def@journalName{ACM Transactions on Database Systems}%
+  \def@journalNameShort{ACM Trans. Datab. Syst.}%
+  \def@permissionCodeOne{0362-5915}%
+\or % TOG
+  \def@journalName{ACM Transactions on Graphics}%
+  \def@journalNameShort{ACM Trans. Graph.}%
+  \def@permissionCodeOne{0730-0301}
+\or % TOIS
+  \def@journalName{ACM Transactions on Information Systems}%
+  \def@permissionCodeOne{1046-8188}%
+\or % TOIT
+  \def@journalName{ACM Transactions on Internet Technology}%
+  \def@journalNameShort{ACM Trans. Internet Technol.}%
+  \def@permissionCodeOne{1533-5399}%
+\or % TOMACS
+  \def@journalName{ACM Transactions on Modeling and Computer Simulation}%
+  \def@journalNameShort{ACM Trans. Model. Comput. Simul.}%
+\or % TOMM
+  \def@journalName{ACM Transactions on Multimedia Computing, Communications and Applications}%
+  \def@journalNameShort{ACM Trans. Multimedia Comput. Commun. Appl.}%
+  \def@permissionCodeOne{1551-6857}%
+  \def@permissionCodeTwo{0100}%
+\or % TOMPECS
+  \def@journalName{ACM Transactions on Modeling and Performance Evaluation of Computing Systems}%
+  \def@journalNameShort{ACM Trans. Model. Perform. Eval. Comput. Syst.}%
+  \def@permissionCodeOne{2376-3639}%
+\or % TOMS
+  \def@journalName{ACM Transactions on Mathematical Software}%
+  \def@journalNameShort{ACM Trans. Math. Softw.}%
+  \def@permissionCodeOne{0098-3500}%
+\or % TOPC
+  \def@journalName{ACM Transactions on Parallel Computing}%
+  \def@journalNameShort{ACM Trans. Parallel Comput.}%
+  \def@permissionCodeOne{1539-9087}%
+\or % TOPS
+  \def@journalName{ACM Transactions on Privacy and Security}%
+  \def@journalNameShort{ACM Trans. Priv. Sec.}%
+  \def@permissionCodeOne{2471-2566}%
+\or % TOPLAS
+  \def@journalName{ACM Transactions on Programming Languages and Systems}%
+  \def@journalNameShort{ACM Trans. Program. Lang. Syst.}%
+  \def@permissionCodeOne{0164-0925}%
+\or % TOS
+  \def@journalName{ACM Transactions on Storage}%
+  \def@journalNameShort{ACM Trans. Storage}%
+  \def@permissionCodeOne{1553-3077}%
+\or % TOSEM
+  \def@journalName{ACM Transactions on Software Engineering and Methodology}%
+  \def@journalNameShort{ACM Trans. Softw. Eng. Methodol.}%
+  \def@permissionCodeOne{1049-331X}%
+\or % TOSN
+  \def@journalName{ACM Transactions on Sensor Networks}%
+  \def@journalNameShort{ACM Trans. Sensor Netw.}%
+  \def@permissionCodeOne{1550-4859}%
+\or % TRETS
+  \def@journalName{ACM Transactions on Reconfigurable Technology and Systems}%
+  \def@journalNameShort{ACM Trans. Reconfig. Technol. Syst.}%
+  \def@permissionCodeOne{1936-7406}%
+\or % TSAS
+  \def@journalName{ACM Transactions on Spatial Algorithms and Systems}%
+  \def@journalNameShort{ACM Trans. Spatial Algorithms Syst.}%
+  \def@permissionCodeOne{2374-0353}%
+\or % TSC
+  \def@journalName{ACM Transactions on Social Computing}%
+  \def@journalNameShort{ACM Trans. Soc. Comput.}%
+  \def@permissionCodeOne{2469-7818}%
+\or % TSLP
+  \def@journalName{ACM Transactions on Speech and Language Processing}%
+  \def@journalNameShort{ACM Trans. Speech Lang. Process.}%
+  \def@permissionCodeOne{1550-4875}%
+\or % TWEB
+  \def@journalName{ACM Transactions on the Web}%
+  \def@journalNameShort{ACM Trans. Web}%
+  \def@permissionCodeOne{1559-1131}%
+\fi
+\ClassInfo{@classname}{Using journal code @journalCode}%
+}{%
+  \ClassError{@classname}{Incorrect journal #1}%
+}%
+\def\acmJournal#1{\setkeys{ACM}{acmJournal=#1}%
+  \global@ACM@journal@bibstriptrue}
+\def@journalCode@nr{0}
+\def@journalName{}%
+\def@journalNameShort{@journalName}%
+\def@permissionCodeOne{XXXX-XXXX}%
+\def@permissionCodeTwo{}%
+\newcommand\acmConference[4][]{%
+  \gdef\acmConference@shortname{#1}%
+  \gdef\acmConference@name{#2}%
+  \gdef\acmConference@date{#3}%
+  \gdef\acmConference@venue{#4}%
+  \ifx\acmConference@shortname@empty
+    \gdef\acmConference@shortname{#2}%
+  \fi
+  \global@ACM@journal@bibstripfalse
+}
+\if@ACM@journal\else
+\acmConference[Conference'17]{ACM Conference}{July 2017}{Washington,
+  DC, USA}%
+\fi
+\def\acmBooktitle#1{\gdef@acmBooktitle{#1}}
+\acmBooktitle{Proceedings of \acmConference@name
+       \ifx\acmConference@name\acmConference@shortname\else
+         \ (\acmConference@shortname)\fi}
+\def@editorsAbbrev{(Ed.)}
+\def@acmEditors{}
+\def\editor#1{\ifx@acmEditors@empty
+    \gdef@acmEditors{#1}%
+  \else
+    \gdef@editorsAbbrev{(Eds.)}%
+    \g@addto@macro@acmEditors{\and#1}%
+\fi}
+\def\subtitle#1{\def@subtitle{#1}}
+\subtitle{}
+\newcount\num@authorgroups
+\num@authorgroups=0\relax
+\newcount\num@authors
+\num@authors=0\relax
+\newif\if@insideauthorgroup
+@insideauthorgroupfalse
+\renewcommand\author[2][]{%
+  \IfSubStr{#2}{,}{\ClassWarning{@classname}{Do not put several
+      authors in the same \string\author\space macro!}}{}%
+  \global\advance\num@authors by 1\relax
+  \if@insideauthorgroup\else
+    \global\advance\num@authorgroups by 1\relax
+    \global@insideauthorgrouptrue
+  \fi
+  \ifx\addresses@empty
+    \if@ACM@anonymous
+      \gdef\addresses{@author{Anonymous Author(s)%
+        \ifx@acmSubmissionID@empty\else\Submission Id:
+          @acmSubmissionID\fi}}%
+      \gdef\authors{Anonymous Author(s)}%
+    \else
+      \gdef\addresses{@author{#2}}%
+      \gdef\authors{#2}%
+    \fi
+  \else
+    \if@ACM@anonymous\else
+      \g@addto@macro\addresses{\and@author{#2}}%
+      \g@addto@macro\authors{\and#2}%
+    \fi
+  \fi
+  \if@ACM@anonymous
+    \ifx\shortauthors@empty
+      \gdef\shortauthors{Anon.
+        \ifx@acmSubmissionID@empty\else Submission Id:
+        @acmSubmissionID\fi}%
+    \fi
+  \else
+    \def@tempa{#1}%
+    \ifx@tempa@empty
+      \ifx\shortauthors@empty
+        \gdef\shortauthors{#2}%
+      \else
+        \g@addto@macro\shortauthors{\and#2}%
+      \fi
+    \else
+      \ifx\shortauthors@empty
+        \gdef\shortauthors{#1}%
+      \else
+        \g@addto@macro\shortauthors{\and#1}%
+      \fi
+    \fi
+  \fi}
+\newcommand{\affiliation}[2][]{%
+  \global@insideauthorgroupfalse
+  \if@ACM@anonymous\else
+    \g@addto@macro\addresses{\affiliation{#1}{#2}}%
+  \fi}
+\define@boolkey+{@ACM@affiliation@}[@ACM@affiliation@]{obeypunctuation}%
+[true]{}{\ClassError{@classname}{The option obeypunctuation can be either true or false}}
+\def\additionalaffiliation#1{\authornote{@additionalaffiliation{#1}}}
+\def@additionalaffiliation#1{\bgroup
+  \def\position##1{\ignorespaces}%
+  \def\institution##1{##1\ignorespaces}%
+  \def\department{@ifnextchar[{@department}{@department[]}}%
+  \def@department[##1]##2{\unskip, ##2\ignorespaces}%
+  \let\streetaddress\position
+  \let\city\position
+  \let\state\position
+  \let\postcode\position
+  \let\country\position
+  Also with #1\unskip.\egroup}
+\renewcommand{\email}[2][]{%
+  \IfSubStr{#2}{,}{\ClassWarning{@classname}{Do not put several
+      addresses in the same \string\email\space macro!}}{}%
+  \if@ACM@anonymous\else
+    \g@addto@macro\addresses{\email{#1}{#2}}%
+  \fi}
+\def\orcid#1{\unskip\ignorespaces}
+\def\authorsaddresses#1{\def@authorsaddresses{#1}}
+\authorsaddresses{@mkauthorsaddresses}
+\def@titlenotes{}
+\def\titlenote#1{%
+  \g@addto@macro@title{\footnotemark}%
+  \if@ACM@anonymous
+    \g@addto@macro@titlenotes{%
+      \stepcounter{footnote}\footnotetext{Title note}}%
+  \else
+    \g@addto@macro@titlenotes{\stepcounter{footnote}\footnotetext{#1}}%
+  \fi}
+\def@subtitlenotes{}
+\def\subtitlenote#1{%
+  \g@addto@macro@subtitle{\footnotemark}%
+  \if@ACM@anonymous
+    \g@addto@macro@subtitlenotes{%
+      \stepcounter{footnote}\footnotetext{Subtitle note}}%
+  \else
+    \g@addto@macro@subtitlenotes{%
+      \stepcounter{footnote}\footnotetext{#1}}%
+  \fi}
+\def@authornotes{}
+\def\authornote#1{%
+  \if@ACM@anonymous\else
+    \g@addto@macro\addresses{@authornotemark}%
+    \g@addto@macro@authornotes{%
+      \stepcounter{footnote}\footnotetext{#1}}%
+  \fi}
+\newcommand\authornotemark[1][\relax]{%
+  \ifx#1\relax\relax\relax
+  \g@addto@macro\addresses{@authornotemark}%
+  \else
+  \g@addto@macro\addresses{@@authornotemark{#1}}%
+  \fi}
+\def\acmVolume#1{\def@acmVolume{#1}}
+\acmVolume{1}
+\def\acmNumber#1{\def@acmNumber{#1}}
+\acmNumber{1}
+\def\acmArticle#1{\def@acmArticle{#1}}
+\acmArticle{}
+\def\acmArticleSeq#1{\def@acmArticleSeq{#1}}
+\acmArticleSeq{@acmArticle}
+\def\acmYear#1{\def@acmYear{#1}}
+\acmYear{\the\year}
+\def\acmMonth#1{\def@acmMonth{#1}}
+\acmMonth{\the\month}
+\def@acmPubDate{\ifcase@acmMonth\or
+  January\or February\or March\or April\or May\or June\or
+  July\or August\or September\or October\or November\or
+  December\fi~@acmYear}
+\def\acmPrice#1{\def@acmPrice{#1}}
+\acmPrice{15.00}
+\def\acmSubmissionID#1{\def@acmSubmissionID{#1}}
+\acmSubmissionID{}
+\def\acmISBN#1{\def@acmISBN{#1}}
+\acmISBN{978-x-xxxx-xxxx-x/YY/MM}
+\def\acmDOI#1{\def@acmDOI{#1}}
+\acmDOI{10.1145/nnnnnnn.nnnnnnn}
+\newif\if@ACM@badge
+@ACM@badgefalse
+\newlength@ACM@badge@width
+\setlength@ACM@badge@width{5pc}
+\newlength@ACM@title@width
+\newlength@ACM@badge@skip
+\setlength@ACM@badge@skip{1pc}
+\newcommand\acmBadgeR[2][]{@ACM@badgetrue
+  \def@acmBadgeR@url{#1}%
+  \def@acmBadgeR@image{#2}}
+\def@acmBadgeR@url{}
+\def@acmBadgeR@image{}
+\newcommand\acmBadgeL[2][]{@ACM@badgetrue
+  \def@acmBadgeL@url{#1}%
+  \def@acmBadgeL@image{#2}}
+\def@acmBadgeL@url{}
+\def@acmBadgeL@image{}
+\def\startPage#1{\def@startPage{#1}}
+\startPage{}
+\def\terms#1{\ClassWarning{@classname}{The command \string\terms{} is
+    obsolete.  I am going to ignore it}}
+\def\keywords#1{\def@keywords{#1}}
+\keywords{}
+\renewenvironment{abstract}{\Collect@Body@saveabstract}{}
+\long\def@saveabstract#1{\long\gdef@abstract{#1}}
+@saveabstract{}
+\long\def@lempty{}
+\define@boolkey+{@ACM@topmatter@}[@ACM@]{printccs}[true]{%
+  \if@ACM@printccs
+    \ClassInfo{@classname}{Printing CCS}%
+  \else
+    \ClassInfo{@classname}{Suppressing CCS}%
+  \fi}{\ClassError{@classname}{The option printccs can be either true or false}}
+\define@boolkey+{@ACM@topmatter@}[@ACM@]{printacmref}[true]{%
+  \if@ACM@printacmref
+    \ClassInfo{@classname}{Printing bibformat}%
+  \else
+    \ClassInfo{@classname}{Suppressing bibformat}%
+  \fi}{\ClassError{@classname}{The option printacmref can be either true or false}}
+\define@boolkey+{@ACM@topmatter@}[@ACM@]{printfolios}[true]{%
+  \if@ACM@printfolios
+    \ClassInfo{@classname}{Printing folios}%
+  \else
+    \ClassInfo{@classname}{Suppressing folios}%
+  \fi}{\ClassError{@classname}{The option printfolios can be either true or false}}
+\define@cmdkey{@ACM@topmatter@}[@ACM@]{authorsperrow}[0]{%
+  \IfInteger{#1}{\ClassInfo{@classname}{Setting authorsperrow to
+      #1}}{\ClassWarning{@classname}{The parameter authorsperrow must be
+      numerical. Ignoring the input #1}\gdef@ACM@authorsperrow{0}}}
+\def\settopmatter#1{\setkeys{@ACM@topmatter@}{#1}}
+\settopmatter{printccs=true, printacmref=true}
+\if@ACM@manuscript
+  \settopmatter{printfolios=true}
+\else
+  \if@ACM@journal
+    \settopmatter{printfolios=true}
+  \else
+    \settopmatter{printfolios=false}
+  \fi
+\fi
+\settopmatter{authorsperrow=0}
+\def@received{}
+\newcommand\received[2][]{\def@tempa{#1}%
+  \ifx@tempa@empty
+    \ifx@received@empty
+      \gdef@received{Received #2}%
+    \else
+      \g@addto@macro{@received}{; revised #2}%
+    \fi
+  \else
+    \ifx@received@empty
+      \gdef@received{#1 #2}%
+    \else
+      \g@addto@macro{@received}{; #1 #2}%
+    \fi
+  \fi}
+\AtEndDocument{%
+  \ifx@received@empty\else
+    \par\bigskip\noindent\small\normalfont@received\par
+  \fi}
+\RequirePackage{comment}
+\excludecomment{CCSXML}
+\let@concepts@empty
+\newcounter{@concepts}
+\newcommand\ccsdesc[2][100]{%
+  \ccsdesc@parse#1~#2~~\ccsdesc@parse@end}
+\RequirePackage{textcomp}
+\def\ccsdesc@parse#1~#2~#3~{%
+  \stepcounter{@concepts}%
+  \expandafter\ifx\csname CCS@General@#2\endcsname\relax
+    \expandafter\gdef\csname CCS@General@#2\endcsname{\textbullet\
+      \textbf{#2}}%
+    \expandafter\gdef\csname CCS@Punctuation@#2\endcsname{; }%
+    \expandafter\gdef\csname CCS@Specific@#2\endcsname{}%
+  \g@addto@macro{@concepts}{\csname CCS@General@#2\endcsname
+    \csname CCS@Punctuation@#2\endcsname
+    \csname CCS@Specific@#2\endcsname}%
+  \fi
+  \ifx#3\relax\relax\else
+    \expandafter\gdef\csname CCS@Punctuation@#2\endcsname{
+      \textrightarrow\ }%
+    \expandafter\g@addto@macro\expandafter{\csname CCS@Specific@#2\endcsname}{%
+     \addtocounter{@concepts}{-1}%
+     \ifnum#1>499\textbf{#3}\else
+     \ifnum#1>299\textit{#3}\else
+     #3\fi\fi\ifnum\value{@concepts}=0.\else; \fi}%
+  \fi
+\ccsdesc@parse@finish}
+\def\ccsdesc@parse@finish#1\ccsdesc@parse@end{}
+\newif\if@printcopyright
+@printcopyrighttrue
+\newif\if@printpermission
+@printpermissiontrue
+\newif\if@acmowned
+@acmownedtrue
+\define@choicekey*{ACM@}{acmcopyrightmode}[%
+  \acm@copyrightinput\acm@copyrightmode]{none,%
+    acmcopyright,acmlicensed,rightsretained,%
+    usgov,usgovmixed,cagov,cagovmixed,licensedusgovmixed,%
+    licensedcagov,licensedcagovmixed,othergov,licensedothergov,%
+    iw3c2w3,iw3c2w3g}{%
+  @printpermissiontrue
+  @printcopyrighttrue
+  @acmownedtrue
+  \ifnum\acm@copyrightmode=0\relax % none
+   @printpermissionfalse
+   @printcopyrightfalse
+   @acmownedfalse
+  \fi
+  \ifnum\acm@copyrightmode=2\relax % acmlicensed
+   @acmownedfalse
+  \fi
+  \ifnum\acm@copyrightmode=3\relax % rightsretained
+   @acmownedfalse
+   \AtBeginDocument{\acmPrice{}}%
+  \fi
+  \ifnum\acm@copyrightmode=4\relax % usgov
+   @printpermissiontrue
+   @printcopyrightfalse
+   @acmownedfalse
+   \AtBeginDocument{\acmPrice{}}%
+  \fi
+  \ifnum\acm@copyrightmode=6\relax % cagov
+   @acmownedfalse
+  \fi
+  \ifnum\acm@copyrightmode=8\relax % licensedusgovmixed
+   @acmownedfalse
+  \fi
+  \ifnum\acm@copyrightmode=9\relax % licensedcagov
+   @acmownedfalse
+  \fi
+  \ifnum\acm@copyrightmode=10\relax % licensedcagovmixed
+   @acmownedfalse
+  \fi
+  \ifnum\acm@copyrightmode=11\relax % othergov
+   @acmownedtrue
+  \fi
+  \ifnum\acm@copyrightmode=12\relax % licensedothergov
+   @acmownedfalse
+  \fi
+  \ifnum\acm@copyrightmode=13\relax % iw3c2w3
+   @acmownedfalse
+   \AtBeginDocument{\acmPrice{}}%
+  \fi
+  \ifnum\acm@copyrightmode=14\relax % iw3c2w3g
+   @acmownedfalse
+   \AtBeginDocument{\acmPrice{}}%
+  \fi}
+\def\setcopyright#1{\setkeys{ACM@}{acmcopyrightmode=#1}}
+\setcopyright{acmcopyright}
+\def@copyrightowner{%
+  \ifcase\acm@copyrightmode\relax % none
+  \or % acmcopyright
+  Association for Computing Machinery.
+  \or % acmlicensed
+  Copyright held by the owner/author(s). Publication rights licensed to
+  ACM@.
+  \or % rightsretained
+  Copyright held by the owner/author(s).
+  \or % usgov
+  \or % usgovmixed
+  Association for Computing Machinery.
+  \or % cagov
+  Crown in Right of Canada.
+  \or %cagovmixed
+  Association for Computing Machinery.
+  \or %licensedusgovmixed
+  Copyright held by the owner/author(s). Publication rights licensed to
+  ACM@.
+  \or % licensedcagov
+  Crown in Right of Canada. Publication rights licensed to
+  ACM@.
+  \or %licensedcagovmixed
+  Copyright held by the owner/author(s). Publication rights licensed to
+  ACM@.
+  \or % othergov
+  Association for Computing Machinery.
+  \or % licensedothergov
+  Copyright held by the owner/author(s). Publication rights licensed to
+  ACM@.
+  \or % ic2w3www
+  IW3C2 (International World Wide Web Conference Committee), published
+  under Creative Commons CC-BY~4.0 License.
+  \or % ic2w3wwwgoogle
+  IW3C2 (International World Wide Web Conference Committee), published
+  under Creative Commons CC-BY-NC-ND~4.0 License.
+  \fi}
+\def@formatdoi#1{\url{https://doi.org/#1%7D%7D
+\def@copyrightpermission{%
+  \ifcase\acm@copyrightmode\relax % none
+  \or % acmcopyright
+   Permission to make digital or hard copies of all or part of this
+   work for personal or classroom use is granted without fee provided
+   that copies are not made or distributed for profit or commercial
+   advantage and that copies bear this notice and the full citation on
+   the first page. Copyrights for components of this work owned by
+   others than ACM must be honored. Abstracting with credit is
+   permitted. To copy otherwise, or republish, to post on servers or to
+   redistribute to lists, requires prior specific permission
+   and\hspace*{.5pt}/or  a fee. Request permissions from
+   permissions@acm.org.
+  \or % acmlicensed
+   Permission to make digital or hard copies of all or part of this
+   work for personal or classroom use is granted without fee provided
+   that copies are not made or distributed for profit or commercial
+   advantage and that copies bear this notice and the full citation on
+   the first page. Copyrights for components of this work owned by
+   others than the author(s) must be honored. Abstracting with credit
+   is permitted.  To copy otherwise, or republish, to post on servers
+   or to  redistribute to lists, requires prior specific permission
+   and\hspace*{.5pt}/or  a fee. Request permissions from
+   permissions@acm.org.
+  \or % rightsretained
+   Permission to make digital or hard copies of part or all of this work
+   for personal or classroom use is granted without fee provided that
+   copies are not made or distributed for profit or commercial advantage
+   and that copies bear this notice and the full citation on the first
+   page. Copyrights for third-party components of this work must be
+   honored. For all other uses, contact the
+   owner\hspace*{.5pt}/author(s).
+  \or % usgov
+   This paper is authored by an employee(s) of the United States
+   Government and is in the public domain. Non-exclusive copying or
+   redistribution is allowed, provided that the article citation is
+   given and the authors and agency are clearly identified as its
+   source.
+  \or % usgovmixed
+   ACM acknowledges that this contribution was authored or co-authored
+   by an employee, contractor, or affiliate of the United States government. As such,
+   the United States government retains a nonexclusive, royalty-free right to
+   publish or reproduce this article, or to allow others to do so, for
+   government purposes only.
+  \or % cagov
+   This article was authored by employees of the Government of Canada.
+   As such, the Canadian government retains all interest in the
+   copyright to this work and grants to ACM a nonexclusive,
+   royalty-free right to publish or reproduce this article, or to allow
+   others to do so, provided that clear attribution is given both to
+   the authors and the Canadian government agency employing them.
+   Permission to make digital or hard copies for personal or classroom
+   use is granted. Copies must bear this notice and the full citation
+   on the first page.  Copyrights for components of this work owned by
+   others than the Canadian Government must be honored. To copy
+   otherwise, distribute, republish, or post, requires prior specific
+   permission and\hspace*{.5pt}/or a fee. Request permissions from
+   permissions@acm.org.
+  \or % cagovmixed
+   ACM acknowledges that this contribution was co-authored by an
+   affiliate of the national government of Canada. As such, the Crown
+   in Right of Canada retains an equal interest in the copyright.
+   Reprints must include clear attribution to ACM and the author's
+   government agency affiliation.  Permission to make digital or hard
+   copies for personal or classroom use is granted.  Copies must bear
+   this notice and the full citation on the first page. Copyrights for
+   components of this work owned by others than ACM must be honored.
+   To copy otherwise, distribute, republish, or post, requires prior
+   specific permission and\hspace*{.5pt}/or a fee. Request permissions
+   from permissions@acm.org.
+  \or % licensedusgovmixed
+   Publication rights licensed to ACM@. ACM acknowledges that this
+   contribution was authored or co-authored by an employee, contractor
+   or affiliate of the United States government. As such, the
+   Government retains a nonexclusive, royalty-free right to publish or
+   reproduce this article, or to allow others to do so, for Government
+   purposes only.
+  \or % licensedcagov
+   This article was authored by employees of the Government of Canada.
+   As such, the Canadian government retains all interest in the
+   copyright to this work and grants to ACM a nonexclusive,
+   royalty-free right to publish or reproduce this article, or to allow
+   others to do so, provided that clear attribution is given both to
+   the authors and the Canadian government agency employing them.
+   Permission to make digital or hard copies for personal or classroom
+   use is granted. Copies must bear this notice and the full citation
+   on the first page.  Copyrights for components of this work owned by
+   others than the Canadian Government must be honored. To copy
+   otherwise, distribute, republish, or post, requires prior specific
+   permission and\hspace*{.5pt}/or a fee. Request permissions from
+   permissions@acm.org.
+  \or % licensedcagovmixed
+   Publication rights licensed to ACM@. ACM acknowledges that this
+   contribution was authored or co-authored by an employee, contractor
+   or affiliate of the national government of Canada. As such, the
+   Government retains a nonexclusive, royalty-free right to publish or
+   reproduce this article, or to allow others to do so, for Government
+   purposes only.
+  \or % othergov
+   ACM acknowledges that this contribution was authored or co-authored
+   by an employee, contractor or affiliate of a national government. As
+   such, the Government retains a nonexclusive, royalty-free right to
+   publish or reproduce this article, or to allow others to do so, for
+   Government purposes only.
+  \or % licensedothergov
+   Publication rights licensed to ACM@. ACM acknowledges that this
+   contribution was authored or co-authored by an employee, contractor
+   or affiliate of a national government. As such, the Government
+   retains a nonexclusive, royalty-free right to publish or reproduce
+   this article, or to allow others to do so, for Government purposes
+   only.
+ \or % iw3c2w3
+   This paper is published under the Creative Commons Attribution~4.0
+   International (CC-BY~4.0) license. Authors reserve their rights to
+   disseminate the work on their personal and corporate Web sites with
+   the appropriate attribution.
+ \or % iw3c2w3g
+   This paper is published under the Creative Commons
+   Attribution-NonCommercial-NoDerivs~4.0 International
+   (CC-BY-NC-ND~4.0) license. Authors reserve their rights to
+   disseminate the work on their personal and corporate Web sites with
+   the appropriate attribution.
+ \fi}
+\def\copyrightyear#1{\def@copyrightyear{#1}}
+\copyrightyear{@acmYear}
+\def@teaserfigures{}
+\newenvironment{teaserfigure}{\Collect@Body@saveteaser}{}
+\long\def@saveteaser#1{\g@addto@macro@teaserfigures{@teaser{#1}}}
+\renewcommand{\thanks}[1]{%
+  @ifnotempty{#1}{%
+    \if@ACM@anonymous
+      \g@addto@macro\thankses{\thanks{A note}}%
+   \else
+    \g@addto@macro\thankses{\thanks{#1}}%
+   \fi}}
+\newbox\mktitle@bx
+\def\maketitle{%
+  \if@ACM@anonymous
+    % Anonymize omission of \author-s
+    \ifnum\num@authorgroups=0\author{}\fi
+  \fi
+  \begingroup
+  \let@vspace@vspace@orig
+  \let@vspacer@vspacer@orig
+  \let@footnotemark@footnotemark@nolink
+  \let@footnotetext@footnotetext@nolink
+  \renewcommand\thefootnote{@fnsymbol\c@footnote}%
+  \hsize=\textwidth
+  \def@makefnmark{\hbox{@textsuperscript{@thefnmark}}}%
+  @mktitle\if@ACM@sigchiamode\else@mkauthors\fi@mkteasers
+  @printtopmatter
+  \if@ACM@sigchiamode@mkauthors\fi
+  \setcounter{footnote}{0}%
+  \def@makefnmark{\hbox{@textsuperscript{\normalfont@thefnmark}}}%
+  @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@bibstrip
+         \footnotetextauthorsaddresses{%
+           \def\par{\let\par@par}\parindent\z@@setauthorsaddresses}%
+       \fi
+     \fi
+  \fi
+  \if@ACM@nonacm\else\footnotetextcopyrightpermission{%
+    \if@ACM@authordraft
+        \raisebox{-2ex}[\z@][\z@]{\makebox[0pt][l]{\large\bfseries
+            Unpublished working draft. Not for distribution.}}%
+       \color[gray]{0.9}%
+    \fi
+    \parindent\z@\parskip0.1\baselineskip
+    \if@ACM@authorversion\else
+      \if@printpermission@copyrightpermission\par\fi
+    \fi
+    \if@ACM@manuscript\else
+       \if@ACM@journal@bibstrip\else % Print the conference information
+         {\itshape \acmConference@shortname, \acmConference@date, \acmConference@venue}\par
+       \fi
+    \fi
+    \if@printcopyright
+      \copyright\ @copyrightyear\ @copyrightowner\
+    \else
+      @copyrightyear.\
+    \fi
+    \if@ACM@manuscript
+      Manuscript submitted to ACM\
+    \else
+      \if@ACM@authorversion
+          This is the author's version of the work. It is posted here for
+          your personal use. Not for redistribution. The definitive Version
+          of Record was published in
+          \if@ACM@journal@bibstrip
+            \emph{@journalName}%
+          \else
+            \emph{@acmBooktitle}%
+          \fi
+          \ifx@acmDOI@empty
+          .
+          \else
+            , @formatdoi{@acmDOI}.
+          \fi\
+        \else
+          \if@ACM@nonacm\else
+            \if@ACM@journal@bibstrip
+              @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
+  \if@ACM@printccs
+  \ifx@concepts@empty\else\bgroup
+      {@specialsection{CCS Concepts}%
+         @concepts\par}\egroup
+     \fi
+   \fi
+   \ifx@keywords@empty\else\bgroup
+      {\if@ACM@journal
+         @specialsection{Additional Key Words and Phrases}%
+       \else
+         @specialsection{Keywords}%
+       \fi
+         @keywords}\par\egroup
+   \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
+}
+\def@specialsection#1{%
+  \ifcase\ACM@format@nr
+  \relax % manuscript
+    \par\medskip\small\noindent#1: %
+  \or % acmsmall
+    \par\medskip\small\noindent#1: %
+  \or % acmlarge
+    \par\medskip\small\noindent#1: %
+  \or % acmtog
+    \par\medskip\small\noindent#1: %
+  \or % sigconf
+    \section*{#1}%
+  \or % siggraph
+    \section*{#1}%
+  \or % sigplan
+    \paragraph*{#1}%
+  \or % sigchi
+    \section*{#1}%
+  \or % sigchi-a
+    \section*{#1}%
+    \fi}
+\def@printtopmatter{%
+  \ifx@startPage@empty
+     \gdef@startPage{1}%
+  \else
+     \setcounter{page}{@startPage}%
+  \fi
+  \thispagestyle{firstpagestyle}%
+  \noindent
+  \ifcase\ACM@format@nr
+  \relax % manuscript
+    \box\mktitle@bx\par
+  \or % acmsmall
+    \box\mktitle@bx\par
+  \or % acmlarge
+    \box\mktitle@bx\par
+  \or % acmtog
+    \twocolumn[\box\mktitle@bx]%
+  \or % sigconf
+    \twocolumn[\box\mktitle@bx]%
+  \or % siggraph
+    \twocolumn[\box\mktitle@bx]%
+  \or % sigplan
+    \twocolumn[\box\mktitle@bx]%
+  \or % sigchi
+    \twocolumn[\box\mktitle@bx]%
+  \or % sigchi-a
+    \par\box\mktitle@bx\par\bigskip
+    \if@ACM@badge
+       \marginpar{\noindent
+         \ifx@acmBadgeL@image@empty\else
+           \href{@acmBadgeL@url}{%
+             \includegraphics[width=@ACM@badge@width]{@acmBadgeL@image}}%
+            \hskip@ACM@badge@skip
+          \fi
+         \ifx@acmBadgeR@image@empty\else
+           \href{@acmBadgeR@url}{%
+             \includegraphics[width=@ACM@badge@width]{@acmBadgeR@image}}%
+          \fi}%
+    \fi
+  \fi
+}
+\def@mktitle{%
+  \ifcase\ACM@format@nr
+  \relax % manuscript
+    @mktitle@i
+  \or % acmsmall
+    @mktitle@i
+  \or % acmlarge
+    @mktitle@i
+  \or % acmtog
+    @mktitle@i
+  \or % sigconf
+    @mktitle@iii
+  \or % siggraph
+    @mktitle@iii
+  \or % sigplan
+    @mktitle@iii
+  \or % sigchi
+    @mktitle@iii
+  \or % sigchi-a
+    @mktitle@iv
+  \fi
+}
+\def@titlefont{%
+  \ifcase\ACM@format@nr
+  \relax % manuscript
+    \LARGE\sffamily\bfseries
+  \or % acmsmall
+    \LARGE\sffamily\bfseries
+  \or % acmlarge
+    \LARGE\sffamily\bfseries
+  \or % acmtog
+    \Huge\sffamily
+  \or % sigconf
+    \Huge\sffamily\bfseries
+  \or % siggraph
+    \Huge\sffamily\bfseries
+  \or % sigplan
+    \Huge\bfseries
+  \or % sigchi
+    \Huge\sffamily\bfseries
+  \or % sigchi-a
+     \Huge\bfseries
+  \fi}
+\def@subtitlefont{\normalsize
+  \ifcase\ACM@format@nr
+  \relax % manuscript
+    \mdseries
+  \or % acmsmall
+    \mdseries
+  \or % acmlarge
+    \mdseries
+  \or % acmtog
+     \LARGE
+  \or % sigconf
+     \LARGE\mdseries
+  \or % siggraph
+     \LARGE\mdseries
+  \or % sigplan
+     \LARGE\mdseries
+  \or % sigchi
+     \LARGE\mdseries
+  \or % sigchi-a
+     \mdseries
+  \fi}
+\def@mktitle@i{\hsize=\textwidth
+  @ACM@title@width=\hsize
+  \ifx@acmBadgeL@image@empty\else
+    \advance@ACM@title@width by -@ACM@badge@width
+    \advance@ACM@title@width by -@ACM@badge@skip
+  \fi
+  \ifx@acmBadgeR@image@empty\else
+    \advance@ACM@title@width by -@ACM@badge@width
+    \advance@ACM@title@width by -@ACM@badge@skip
+  \fi
+  \setbox\mktitle@bx=\vbox{\noindent@titlefont
+    \ifx@acmBadgeL@image@empty\else
+      \raisebox{-.5\baselineskip}[\z@][\z@]{\href{@acmBadgeL@url}{%
+          \includegraphics[width=@ACM@badge@width]{@acmBadgeL@image}}}%
+      \hskip@ACM@badge@skip
+    \fi
+    \parbox[t]{@ACM@title@width}{\raggedright
+      @titlefont\noindent
+      @title
+  \ifx@subtitle@empty\else
+    \par\noindent{@subtitlefont@subtitle}
+  \fi}%
+  \ifx@acmBadgeR@image@empty\else
+    \hskip@ACM@badge@skip
+    \raisebox{-.5\baselineskip}[\z@][\z@]{\href{@acmBadgeR@url}{%
+        \includegraphics[width=@ACM@badge@width]{@acmBadgeR@image}}}%
+  \fi
+  \par\bigskip}}%
+\def@mktitle@iii{\hsize=\textwidth
+    \setbox\mktitle@bx=\vbox{@titlefont\centering
+      @ACM@title@width=\hsize
+      \if@ACM@badge
+        \advance@ACM@title@width by -2@ACM@badge@width
+        \advance@ACM@title@width by -2@ACM@badge@skip
+        \parbox[b]{@ACM@badge@width}{\strut
+          \ifx@acmBadgeL@image@empty\else
+            \raisebox{-.5\baselineskip}[\z@][\z@]{\href{@acmBadgeL@url}{%
+                \includegraphics[width=@ACM@badge@width]{@acmBadgeL@image}}}%
+          \fi}%
+        \hskip@ACM@badge@skip
+      \fi
+      \parbox[t]{@ACM@title@width}{\centering@titlefont
+        @title
+        \ifx@subtitle@empty\else
+          \par\noindent{@subtitlefont@subtitle}
+        \fi
+      }%
+      \if@ACM@badge
+        \hskip@ACM@badge@skip
+        \parbox[b]{@ACM@badge@width}{\strut
+          \ifx@acmBadgeR@image@empty\else
+            \raisebox{-.5\baselineskip}[\z@][\z@]{\href{@acmBadgeR@url}{%
+                \includegraphics[width=@ACM@badge@width]{@acmBadgeR@image}}}%
+          \fi}%
+      \fi
+      \par\bigskip}}%
+\def@mktitle@iv{\hsize=\textwidth
+    \setbox\mktitle@bx=\vbox{\raggedright\leftskip5pc@titlefont
+      \noindent\leavevmode\leaders\hrule height 2pt\hfill\kern0pt\par
+      \noindent@title
+     \ifx@subtitle@empty\else
+       \par\noindent@subtitlefont@subtitle
+     \fi
+     \par\bigskip}}%
+\newbox@ACM@commabox
+\def@ACM@addtoaddress#1{%
+  \ifvmode\else
+    \if@ACM@affiliation@obeypunctuation\else
+    \setbox@ACM@commabox=\hbox{, }%
+    \unskip\cleaders\copy@ACM@commabox\hskip\wd@ACM@commabox
+  \fi\fi
+  #1}
+\def\streetaddress#1{\unskip\ignorespaces}
+\def\postcode#1{\unskip\ignorespaces}
+\if@ACM@journal
+  \def\position#1{\unskip\ignorespaces}
+  \def\institution#1{\unskip~#1\ignorespaces}
+  \def\city#1{\unskip\ignorespaces}
+  \def\state#1{\unskip\ignorespaces}
+  \newcommand\department[2][0]{\unskip\ignorespaces}
+  \def\country#1{\if@ACM@affiliation@obeypunctuation\else, \fi#1\ignorespaces}
+\else
+  \def\position#1{\if@ACM@affiliation@obeypunctuation#1\else#1\par\fi}%
+  \def\institution#1{\if@ACM@affiliation@obeypunctuation#1\else#1\par\fi}%
+  \newcommand\department[2][0]{\if@ACM@affiliation@obeypunctuation
+    #2\else#2\par\fi}%
+  \let\city@ACM@addtoaddress
+  \let\state@ACM@addtoaddress
+  \let\country@ACM@addtoaddress
+\fi
+\def@mkauthors{\begingroup
+  \hsize=\textwidth
+  \ifcase\ACM@format@nr
+  \relax % manuscript
+    @mkauthors@i
+  \or % acmsmall
+    @mkauthors@i
+  \or % acmlarge
+    @mkauthors@i
+  \or % acmtog
+    @mkauthors@i
+  \or % sigconf
+    @mkauthors@iii
+  \or % siggraph
+    @mkauthors@iii
+  \or % sigplan
+    @mkauthors@iii
+  \or % sigchi
+    @mkauthors@iii
+  \or % sigchi-a
+    @mkauthors@iv
+  \fi
+  \endgroup
+}
+\def@authorfont{\Large\sffamily}
+\def@affiliationfont{\normalsize\normalfont}
+\ifcase\ACM@format@nr
+\relax % manuscript
+\or % acmsmall
+  \def@authorfont{\large\sffamily}
+  \def@affiliationfont{\small\normalfont}
+\or % acmlarge
+\or % acmtog
+  \def@authorfont{\LARGE\sffamily}
+  \def@affiliationfont{\large}
+\or % sigconf
+  \def@authorfont{\LARGE}
+  \def@affiliationfont{\large}
+\or % siggraph
+  \def@authorfont{\normalsize\normalfont}
+  \def@affiliationfont{\normalsize\normalfont}
+\or % sigplan
+  \def@authorfont{\Large\normalfont}
+  \def@affiliationfont{\normalsize\normalfont}
+\or % sigchi
+  \def@authorfont{\bfseries}
+  \def@affiliationfont{\mdseries}
+\or % sigchi-a
+  \def@authorfont{\bfseries}
+  \def@affiliationfont{\mdseries}
+\fi
+\def@typeset@author@line{%
+  \andify@currentauthors\par\noindent
+  @currentauthors\def@currentauthors{}%
+  \ifx@currentaffiliations@empty\else
+    \andify@currentaffiliations
+      \unskip, {@currentaffiliations}\par
+  \fi
+  \def@currentaffiliations{}}
+\def@mkauthors@i{%
+  \def@currentauthors{}%
+  \def@currentaffiliations{}%
+  \global\let\and@typeset@author@line
+  \def@author##1{%
+    \ifx@currentauthors@empty
+      \gdef@currentauthors{@authorfont\MakeTextUppercase{##1}}%
+    \else
+       \g@addto@macro{@currentauthors}{\and\MakeTextUppercase{##1}}%
+    \fi
+    \gdef\and{}}%
+  \def\email##1##2{}%
+  \def\affiliation##1##2{%
+    \def@tempa{##2}\ifx@tempa@empty\else
+       \ifx@currentaffiliations@empty
+          \gdef@currentaffiliations{%
+            \setkeys{@ACM@affiliation@}{obeypunctuation=false}%
+            \setkeys{@ACM@affiliation@}{##1}%
+            @affiliationfont##2}%
+       \else
+         \g@addto@macro{@currentaffiliations}{\and
+           \setkeys{@ACM@affiliation@}{obeypunctuation=false}%
+           \setkeys{@ACM@affiliation@}{##1}##2}%
+      \fi
+    \fi
+     \global\let\and@typeset@author@line}%
+  \global\setbox\mktitle@bx=\vbox{\noindent\box\mktitle@bx\par\medskip
+    \noindent\addresses@typeset@author@line
+   \par\medskip}%
+}
+\newbox\author@bx
+\newdimen\author@bx@wd
+\newskip\author@bx@sep
+\author@bx@sep=1pc\relax
+\def@typeset@author@bx{\bgroup\hsize=\author@bx@wd
+  \def\and{\par}\normalbaselines
+  \global\setbox\author@bx=\vtop{\if@ACM@sigchiamode\else\centering\fi
+    @authorfont@currentauthors\par@affiliationfont
+    @currentaffiliation}\egroup
+  \box\author@bx\hspace{\author@bx@sep}%
+  \gdef@currentauthors{}%
+  \gdef@currentaffiliation{}}
+\def@mkauthors@iii{%
+  \author@bx@wd=\textwidth\relax
+  \advance\author@bx@wd by -\author@bx@sep\relax
+  \ifnum@ACM@authorsperrow>0\relax
+    \divide\author@bx@wd by @ACM@authorsperrow\relax
+  \else
+    \ifcase\num@authorgroups
+    \relax % 0?
+    \or  % 1=one author per row
+    \or  % 2=two authors per row
+       \divide\author@bx@wd by \num@authorgroups\relax
+    \or  % 3=three authors per row
+       \divide\author@bx@wd by \num@authorgroups\relax
+    \or  % 4=two authors per row (!)
+       \divide\author@bx@wd by 2\relax
+    \else % three authors per row
+       \divide\author@bx@wd by 3\relax
+    \fi
+  \fi
+  \advance\author@bx@wd by -\author@bx@sep\relax
+  \gdef@currentauthors{}%
+  \gdef@currentaffiliation{}%
+  \def@author##1{\ifx@currentauthors@empty
+    \gdef@currentauthors{\par##1}%
+  \else
+    \g@addto@macro@currentauthors{\par##1}%
+  \fi
+  \gdef\and{}}%
+  \def\email##1##2{\ifx@currentaffiliation@empty
+    \gdef@currentaffiliation{\bgroup
+      \mathchardef\UrlBreakPenalty=10000\nolinkurl{##2}\egroup}%
+  \else
+    \g@addto@macro@currentaffiliation{\par\bgroup
+      \mathchardef\UrlBreakPenalty=10000\nolinkurl{##2}\egroup}%
+  \fi}%
+  \def\affiliation##1##2{\ifx@currentaffiliation@empty
+    \gdef@currentaffiliation{%
+      \setkeys{@ACM@affiliation@}{obeypunctuation=false}%
+      \setkeys{@ACM@affiliation@}{##1}##2}%
+  \else
+    \g@addto@macro@currentaffiliation{\par
+      \setkeys{@ACM@affiliation@}{obeypunctuation=false}%
+      \setkeys{@ACM@affiliation@}{##1}##2}%
+  \fi
+  \global\let\and@typeset@author@bx
+}%
+  \hsize=\textwidth
+  \global\setbox\mktitle@bx=\vbox{\noindent
+    \box\mktitle@bx\par\medskip\leavevmode
+    \lineskip=1pc\relax\centering\hspace*{-1em}%
+    \addresses\let\and@typeset@author@bx\and\par\bigskip}}
+\def@mkauthors@iv{%
+  \author@bx@wd=\columnwidth\relax
+  \advance\author@bx@wd by -\author@bx@sep\relax
+  \ifnum@ACM@authorsperrow>0\relax
+    \divide\author@bx@wd by @ACM@authorsperrow\relax
+  \else
+    \ifcase\num@authorgroups
+    \relax % 0?
+    \or  % 1=one author per row
+    \else  % 2=two authors per row
+       \divide\author@bx@wd by 2\relax
+    \fi
+  \fi
+  \advance\author@bx@wd by -\author@bx@sep\relax
+  \gdef@currentauthors{}%
+  \gdef@currentaffiliation{}%
+  \def@author##1{\ifx@currentauthors@empty
+    \gdef@currentauthors{\par##1}%
+  \else
+    \g@addto@macro@currentauthors{\par##1}%
+  \fi
+  \gdef\and{}}%
+  \def\email##1##2{\ifx@currentaffiliation@empty
+    \gdef@currentaffiliation{\nolinkurl{##2}}%
+  \else
+    \g@addto@macro@currentaffiliation{\par\nolinkurl{##2}}%
+  \fi}%
+  \def\affiliation##1##2{\ifx@currentaffiliation@empty
+    \gdef@currentaffiliation{%
+      \setkeys{@ACM@affiliation@}{obeypunctuation=false}%
+           \setkeys{@ACM@affiliation@}{##1}##2}%
+  \else
+    \g@addto@macro@currentaffiliation{\par
+      \setkeys{@ACM@affiliation@}{obeypunctuation=false}%
+      \setkeys{@ACM@affiliation@}{##1}##2}%
+  \fi
+  \global\let\and@typeset@author@bx}%
+    \bgroup\hsize=\columnwidth
+    \par\raggedright\leftskip=\z@
+    \lineskip=1pc\noindent
+    \addresses\let\and@typeset@author@bx\and\par\bigskip\egroup}
+\def@mkauthorsaddresses{%
+  \ifnum\num@authors>1\relax
+  Authors' \else Author's \fi
+  \ifnum\num@authorgroups>1\relax
+  addresses: \else address: \fi
+  \bgroup
+  \def\streetaddress##1{\unskip@addpunct, ##1}%
+  \def\postcode##1{\unskip@addpunct, ##1}%
+  \def\position##1{\unskip\ignorespaces}%
+  \def\institution##1{\unskip@addpunct, ##1}%
+  \def\city##1{\unskip@addpunct, ##1}%
+  \def\state##1{\unskip@addpunct, ##1}%
+  \renewcommand\department[2][0]{\unskip@addpunct, ##2}%
+  \def\country##1{\unskip@addpunct, ##1}%
+  \def\and{\unskip@addpunct; }%
+  \def@author##1{##1}%
+  \def\email##1##2{\unskip@addpunct, \nolinkurl{##2}}%
+  \addresses
+  \egroup}
+\def@setaddresses{}
+\def@authornotemark{\g@addto@macro@currentauthors{\footnotemark\relax}}
+\def@@authornotemark#1{\g@addto@macro@currentauthors{\footnotemark[#1]}}
+\def@mkteasers{%
+  \ifx@teaserfigures@empty\else
+    \def@teaser##1{\par\bigskip\bgroup
+      \captionsetup{type=figure}##1\egroup\par}
+    \global\setbox\mktitle@bx=\vbox{\noindent\box\mktitle@bx\par
+      \noindent@Description@presentfalse
+      @teaserfigures\par\if@Description@present\else
+         \global@undescribed@imagestrue
+         \ClassWarning{@classname}{A possible image without
+           description}\fi
+    \medskip}%
+  \fi}
+\def@mkabstract{\bgroup
+  \ifx@abstract@lempty\else
+  {\phantomsection\addcontentsline{toc}{section}{Abstract}%
+    \if@ACM@journal
+       \everypar{\setbox\z@\lastbox\everypar{}}\small
+    \else
+      \section*{\abstractname}%
+    \fi
+   \ignorespaces@abstract\par}%
+  \fi\egroup}
+\def@mkbibcitation{\bgroup
+  \let@vspace@vspace@orig
+  \let@vspacer@vspacer@orig
+  \def@pages@word{\ifnum\getrefnumber{TotPages}=1\relax page\else pages\fi}%
+  \def\footnotemark{}%
+  \def\{\unskip{} \ignorespaces}%
+  \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,
+    Article~@acmArticle\ \fi}%
+  \par\medskip\small\noindent{\bfseries ACM Reference Format:}\par\nobreak
+  \noindent\bgroup
+    \def\{\unskip{}, \ignorespaces}\authors\egroup. @acmYear. @title
+  \ifx@subtitle@empty. \else: @subtitle. \fi
+  \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@bibstrip
+       \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}
+\def@printendtopmatter{\bgroup
+  \let@vspace@vspace@orig
+  \let@vspacer@vspacer@orig
+  \par\bigskip
+  \egroup}
+\def@setthanks{\long\def\thanks##1{\par##1@addpunct.}\thankses}
+\def@setauthorsaddresses{@authorsaddresses\unskip@addpunct.}
+\RequirePackage{fancyhdr}
+\let\ACM@ps@plain\ps@plain
+\let\ACM@ps@myheadings\ps@myheadings
+\let\ACM@ps@headings\ps@headings
+\def\ACM@restore@pagestyle{%
+  \let\ps@plain\ACM@ps@plain
+  \let\ps@myheadings\ACM@ps@myheadings
+  \let\ps@headings\ACM@ps@headings}
+\AtBeginDocument{\ACM@restore@pagestyle}
+\if@ACM@review
+  \newsavebox{\ACM@linecount@bx}
+  \newlength\ACM@linecount@bxht
+  \newcount\ACM@linecount
+  \ACM@linecount@ne\relax
+  \def\ACM@mk@linecount{%
+    \savebox{\ACM@linecount@bx}[4em][t]{\parbox[t]{4em}{%
+        \setlength{\ACM@linecount@bxht}{0pt}%
+        \loop{\color{red}\scriptsize\the\ACM@linecount}\
+        \global\advance\ACM@linecount by @ne
+        \addtolength{\ACM@linecount@bxht}{\baselineskip}%
+        \ifdim\ACM@linecount@bxht<\textheight\repeat
+        {\color{red}\scriptsize\the\ACM@linecount}\hfill
+        \global\advance\ACM@linecount by @ne}}}
+\fi
+\def\ACM@linecountL{%
+  \if@ACM@review
+  \ACM@mk@linecount
+  \begin{picture}(0,0)%
+    \put(-26,-22){\usebox{\ACM@linecount@bx}}%
+  \end{picture}%
+  \fi}
+\def\ACM@linecountR{%
+  \if@ACM@review
+  \ACM@mk@linecount
+  \begin{picture}(0,0)%
+    \put(20,-22){\usebox{\ACM@linecount@bx}}%
+  \end{picture}%
+  \fi}
+\if@ACM@timestamp
+  % Subtracting 30 from \time gives us the effect of rounding down despite
+  % \numexpr rounding to nearest
+  \newcounter{ACM@time@hours}
+  \setcounter{ACM@time@hours}{\numexpr (\time - 30) / 60 \relax}
+  \newcounter{ACM@time@minutes}
+  \setcounter{ACM@time@minutes}{\numexpr \time - \theACM@time@hours * 60 \relax}
+  \newcommand\ACM@timestamp{%
+    \footnotesize%
+    \ifx@acmSubmissionID@empty\relax\else
+    Submission ID: @acmSubmissionID.{ }%
+    \fi
+    \the\year-\two@digits{\the\month}-\two@digits{\the\day}{ }%
+    \two@digits{\theACM@time@hours}:\two@digits{\theACM@time@minutes}{. }%
+    Page \thepage\ of @startPage--\pageref*{TotPages}.%
+  }
+\fi
+\def@shortauthors{%
+  \if@ACM@anonymous
+    Anon.
+    \ifx@acmSubmissionID@empty\else Submission Id: @acmSubmissionID\fi
+  \else\shortauthors\fi}
+\def@headfootfont{\sffamily\footnotesize}
+\AtBeginDocument{%
+\fancypagestyle{standardpagestyle}{%
+  \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%
+  }%
+  \if@ACM@journal@bibstrip
+    \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}%
+      \if@ACM@nonacm\else%
+        \fancyfoot[RO,LE]{\footnotesize Manuscript submitted to ACM}
+      \fi%
+    \or % acmsmall
+      \fancyhead[LE]{\ACM@linecountL@headfootfont@acmArticlePage}%
+      \fancyhead[RO]{@headfootfont@acmArticlePage}%
+      \fancyhead[RE]{@headfootfont@shortauthors}%
+      \fancyhead[LO]{\ACM@linecountL@headfootfont\shorttitle}%
+      \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
+      @acmArticlePage\quad\textbullet\quad@shortauthors}%
+      \fancyhead[LO]{\ACM@linecountL}%
+      \fancyhead[RO]{@headfootfont
+        \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
+        @acmArticlePage\quad\textbullet\quad@shortauthors}%
+      \fancyhead[LO]{\ACM@linecountL}%
+      \fancyhead[RE]{\ACM@linecountR}%
+      \fancyhead[RO]{@headfootfont
+        \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}%
+      \if@ACM@nonacm\else%
+        \fancyhead[LE]{\ACM@linecountL@headfootfont\footnotesize
+          \acmConference@shortname,
+          \acmConference@date, \acmConference@venue}%
+        \fancyhead[RO]{@headfootfont
+          \acmConference@shortname,
+          \acmConference@date, \acmConference@venue\ACM@linecountR}%
+      \fi
+    \fi
+  \else % Proceedings
+    \fancyfoot[C]{\if@ACM@printfolios\footnotesize\thepage\fi}%
+    \fancyhead[LO]{\ACM@linecountL@headfootfont\shorttitle}%
+    \fancyhead[RE]{@headfootfont@shortauthors\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)}%
+  \fi
+  \if@ACM@timestamp
+     \fancyfoot[LO,RE]{\ACM@timestamp}
+  \fi
+}%
+\pagestyle{standardpagestyle}
+}
+\newdimen@folio@wd
+@folio@wd=\z@
+\newdimen@folio@ht
+@folio@ht=\z@
+\newdimen@folio@voffset
+@folio@voffset=\z@
+\def@folio@max{1}
+\ifcase\ACM@format@nr
+\relax % manuscript
+\or % acmsmall
+  @folio@wd=45.75pt\relax
+  @folio@ht=1.25in\relax
+  @folio@voffset=.2in\relax
+  \def@folio@max{8}
+\or % acmlarge
+  @folio@wd=43.25pt\relax
+  @folio@ht=79pt\relax
+  @folio@voffset=.55in\relax
+  \def@folio@max{10}
+\fi
+\def@folioblob{@tempcnta=0@acmArticleSeq\relax
+  \ifnum@tempcnta=0\relax\else
+  \loop
+     \ifnum@tempcnta>@folio@max\relax
+      \advance@tempcnta by - @folio@max
+   \repeat
+    \advance@tempcnta by -1\relax
+    @tempdima=@folio@ht\relax
+    \multiply@tempdima by \the@tempcnta\relax
+    \advance@tempdima by -@folio@voffset\relax
+    \begin{picture}(0,0)
+    \makebox[\z@]{\raisebox{-@tempdima}{%
+        \rlap{%
+          \raisebox{-0.45@folio@ht}[\z@][\z@]{%
+            \rule{@folio@wd}{@folio@ht}}}%
+        \parbox{@folio@wd}{%
+          \centering
+          \textcolor{white}{\LARGE\sffamily\bfseries@acmArticle}}}}
+  \end{picture}\fi}
+
+\AtBeginDocument{%
+\fancypagestyle{firstpagestyle}{%
+  \fancyhf{}%
+  \renewcommand{\headrulewidth}{\z@}%
+  \renewcommand{\footrulewidth}{\z@}%
+  \if@ACM@journal@bibstrip
+    \ifcase\ACM@format@nr
+    \relax % manuscript
+      \fancyhead[L]{\ACM@linecountL}%
+      \fancyfoot[RO,LE]{\if@ACM@printfolios\small\thepage\fi}%
+      \if@ACM@nonacm\else%
+        \fancyfoot[RE,LO]{\footnotesize Manuscript submitted to ACM}%
+      \fi%
+    \or % acmsmall
+      \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
+      \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
+      \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
+      \fancyhead[L]{\ACM@linecountL}%
+      \fancyhead[R]{\ACM@linecountR}%
+      \fancyfoot[C]{\if@ACM@printfolios\footnotesize\thepage\fi}%
+    \fi
+  \else
+    \fancyhead[L]{\ACM@linecountL}%
+    \fancyhead[R]{\ACM@linecountR}%
+    \fancyfoot[C]{\if@ACM@printfolios\footnotesize\thepage\fi}%
+  \fi
+  \if@ACM@timestamp
+    \ifnum\ACM@format@nr=0\relax % Manuscript
+    \fancyfoot[LO,RE]{\ACM@timestamp\quad
+      \if@ACM@nonacm\else
+        \footnotesize Manuscript submitted to ACM
+      \fi}
+    \else
+    \fancyfoot[LO,RE]{\ACM@timestamp}
+    \fi
+  \fi
+}}
+\def\ACM@NRadjust#1{%
+ \begingroup
+  \expandafter\ifx\csname Sectionformat\endcsname\relax
+  % do nothing when  \Sectionformat  is unknown
+   \def\next{\endgroup #1}%
+ \else
+  \def\next{\endgroup
+   \let\realSectionformat\Sectionformat
+   \def\ACM@sect@format@{#1}%
+   \let\Sectionformat\ACM@NR@adjustedSectionformat
+ %%  next lines added 2018-06-17 to ensure section number is styled
+   \let\real@adddotafter@adddotafter
+   \let@adddotafter\ACM@adddotafter
+   #1{}% imposes the styles, but nullifies  \MakeUppercase
+   \let@adddotafter\real@adddotafter
+  }%
+ \fi \next
+}
+\def\ACM@NR@adjustedSectionformat#1#2{%
+ \realSectionformat{\ACM@sect@format{#1}}{#2}%
+ \let\Sectionformat\realSectionformat}
+\DeclareRobustCommand{\ACM@sect@format}{\ACM@sect@format@}
+\def\ACM@sect@format@null#1{#1}
+\let\ACM@sect@format@\ACM@sect@format@null
+\AtBeginDocument{%
+ \expandafter\ifx\csname LTX@adddotafter\endcsname\relax
+  \let\LTX@adddotafter@adddotafter
+ \fi
+}
+\def\ACM@adddotafter#1{\ifx\relax#1\relax\else\LTX@adddotafter{#1}\fi}
+\renewcommand\section{@startsection{section}{1}{\z@}%
+  {-.75\baselineskip @plus -2\p@ @minus -.2\p@}%
+  {.25\baselineskip}%
+  {\ACM@NRadjust@secfont}}
+\renewcommand\subsection{@startsection{subsection}{2}{\z@}%
+  {-.75\baselineskip @plus -2\p@ @minus -.2\p@}%
+  {.25\baselineskip}%
+  {\ACM@NRadjust@subsecfont}}
+\renewcommand\subsubsection{@startsection{subsubsection}{3}{\z@}%
+  {-.5\baselineskip @plus -2\p@ @minus -.2\p@}%
+  {-3.5\p@}%
+  {\ACM@NRadjust{@subsubsecfont@adddotafter}}}
+\renewcommand\paragraph{@startsection{paragraph}{4}{\parindent}%
+  {-.5\baselineskip @plus -2\p@ @minus -.2\p@}%
+  {-3.5\p@}%
+  {\ACM@NRadjust{@parfont@adddotafter}}}
+\renewcommand\part{@startsection{part}{9}{\z@}%
+  {-10\p@ @plus -4\p@ @minus -2\p@}%
+  {4\p@}%
+  {\ACM@NRadjust@parfont}}
+\def\section@raggedright{@rightskip@flushglue
+  \rightskip@rightskip
+  \leftskip\z@skip
+  \parindent\z@}
+\def@secfont{\sffamily\bfseries\section@raggedright\MakeTextUppercase}
+\def@subsecfont{\sffamily\bfseries\section@raggedright}
+\def@subsubsecfont{\sffamily\itshape}
+\def@parfont{\itshape}
+\setcounter{secnumdepth}{3}
+\ifcase\ACM@format@nr
+\relax % manuscript
+\or % acmsmall
+\or % acmlarge
+ \def@secfont{\sffamily\large\section@raggedright\MakeTextUppercase}
+ \def@subsecfont{\sffamily\large\section@raggedright}
+\or % acmtog
+ \def@secfont{\sffamily\large\section@raggedright\MakeTextUppercase}
+ \def@subsecfont{\sffamily\large\section@raggedright}
+\or % sigconf
+ \def@secfont{\bfseries\Large\section@raggedright\MakeTextUppercase}
+ \def@subsecfont{\bfseries\Large\section@raggedright}
+\or % siggraph
+ \def@secfont{\sffamily\bfseries\Large\section@raggedright\MakeTextUppercase}
+ \def@subsecfont{\sffamily\bfseries\Large\section@raggedright}
+\or % sigplan
+ \def@secfont{\bfseries\Large\section@raggedright}
+ \def@subsecfont{\bfseries\section@raggedright}
+ \renewcommand\subsubsection{@startsection{subsubsection}{3}{\z@}%
+   {-.75\baselineskip @plus -2\p@ @minus -.2\p@}%
+   {.25\baselineskip}%
+   {@subsubsecfont}}
+ \def@subsubsecfont{\bfseries\section@raggedright}
+ \renewcommand\paragraph{@startsection{paragraph}{4}{\z@}%
+   {-.5\baselineskip @plus -2\p@ @minus -.2\p@}%
+   {-3.5\p@}%
+   {@parfont@addspaceafter}}
+ \def@parfont{\bfseries\itshape}
+ \renewcommand\subparagraph{@startsection{subparagraph}{5}{\z@}%
+   {-.5\baselineskip @plus -2\p@ @minus -.2\p@}%
+   {-3.5\p@}%
+   {@subparfont@addspaceafter}}
+ \def@subparfont{\itshape}
+\or % sigchi
+ \setcounter{secnumdepth}{1}
+ \def@secfont{\sffamily\bfseries\section@raggedright\MakeTextUppercase}
+ \def@subsecfont{\sffamily\bfseries\section@raggedright}
+\or % sigchi-a
+ \setcounter{secnumdepth}{0}
+ \def@secfont{\sffamily\bfseries\section@raggedright\MakeTextUppercase}
+ \def@subsecfont{\sffamily\bfseries\section@raggedright}
+\fi
+\def@adddotafter#1{#1@addpunct{.}}
+\def@addspaceafter#1{#1@addpunct{\enspace}}
+\providecommand*@dotsep{4.5}
+\def@acmplainbodyfont{\itshape}
+\def@acmplainindent{\parindent}
+\def@acmplainheadfont{\scshape}
+\def@acmplainnotefont{@empty}
+\ifcase\ACM@format@nr
+\relax % manuscript
+\or % acmsmall
+\or % acmlarge
+\or % acmtog
+\or % sigconf
+\or % siggraph
+\or % sigplan
+  \def@acmplainbodyfont{\itshape}
+  \def@acmplainindent{\z@}
+  \def@acmplainheadfont{\bfseries}
+  \def@acmplainnotefont{\normalfont}
+\or % sigchi
+\or % sigchi-a
+\fi
+\newtheoremstyle{acmplain}%
+  {.5\baselineskip@plus.2\baselineskip
+    @minus.2\baselineskip}% space above
+  {.5\baselineskip@plus.2\baselineskip
+    @minus.2\baselineskip}% space below
+  {@acmplainbodyfont}% body font
+  {@acmplainindent}% indent amount
+  {@acmplainheadfont}% head font
+  {.}% punctuation after head
+  {.5em}% spacing after head
+  {\thmname{#1}\thmnumber{ #2}\thmnote{ {@acmplainnotefont(#3)}}}% head spec
+\def@acmdefinitionbodyfont{\normalfont}
+\def@acmdefinitionindent{\parindent}
+\def@acmdefinitionheadfont{\itshape}
+\def@acmdefinitionnotefont{@empty}
+\ifcase\ACM@format@nr
+\relax % manuscript
+\or % acmsmall
+\or % acmlarge
+\or % acmtog
+\or % sigconf
+\or % siggraph
+\or % sigplan
+  \def@acmdefinitionbodyfont{\normalfont}
+  \def@acmdefinitionindent{\z@}
+  \def@acmdefinitionheadfont{\bfseries}
+  \def@acmdefinitionnotefont{\normalfont}
+\or % sigchi
+\or % sigchi-a
+\fi
+\newtheoremstyle{acmdefinition}%
+  {.5\baselineskip@plus.2\baselineskip
+    @minus.2\baselineskip}% space above
+  {.5\baselineskip@plus.2\baselineskip
+    @minus.2\baselineskip}% space below
+  {@acmdefinitionbodyfont}% body font
+  {@acmdefinitionindent}% indent amount
+  {@acmdefinitionheadfont}% head font
+  {.}% punctuation after head
+  {.5em}% spacing after head
+  {\thmname{#1}\thmnumber{ #2}\thmnote{ {@acmdefinitionnotefont(#3)}}}% head spec
+\theoremstyle{acmplain}
+\AtEndPreamble{%
+  \if@ACM@acmthm
+  \theoremstyle{acmplain}
+  @ifundefined{theorem}{%
+  \newtheorem{theorem}{Theorem}[section]
+  }{}
+  @ifundefined{conjecture}{%
+  \newtheorem{conjecture}[theorem]{Conjecture}
+  }{}
+  @ifundefined{proposition}{%
+  \newtheorem{proposition}[theorem]{Proposition}
+  }{}
+  @ifundefined{lemma}{%
+  \newtheorem{lemma}[theorem]{Lemma}
+  }{}
+  @ifundefined{corollary}{%
+  \newtheorem{corollary}[theorem]{Corollary}
+  }{}
+  \theoremstyle{acmdefinition}
+  @ifundefined{example}{%
+  \newtheorem{example}[theorem]{Example}
+  }{}
+  @ifundefined{definition}{%
+  \newtheorem{definition}[theorem]{Definition}
+  }{}
+  \fi
+  \theoremstyle{acmplain}
+}
+\def@proofnamefont{\scshape}
+\def@proofindent{\indent}
+\ifcase\ACM@format@nr
+\relax % manuscript
+\or % acmsmall
+\or % acmlarge
+\or % acmtog
+\or % sigconf
+\or % siggraph
+\or % sigplan
+  \def@proofnamefont{\itshape}
+  \def@proofindent{\noindent}
+\or % sigchi
+\or % sigchi-a
+\fi
+\renewenvironment{proof}[1][\proofname]{\par
+  \pushQED{\qed}%
+  \normalfont \topsep6\p@@plus6\p@\relax
+  \trivlist
+  \item[@proofindent\hskip\labelsep
+        {@proofnamefont #1@addpunct{.}}]\ignorespaces
+}{%
+  \popQED\endtrivlist@endpefalse
+}
+\AtEndPreamble{%
+  \if@ACM@balance
+    \ifcase\ACM@format@nr
+    \relax % manuscript
+         \global@ACM@balancefalse
+       \or % acmsmall
+         \global@ACM@balancefalse
+       \or % acmlarge
+         \global@ACM@balancefalse
+       \or % acmtog
+          \RequirePackage{balance}%
+       \or % sigconf
+          \RequirePackage{balance}%
+       \or % siggraph
+          \RequirePackage{balance}%
+       \or % sigplan
+          \RequirePackage{balance}%
+       \or % sigchi
+          \RequirePackage{balance}%
+       \or % sigchi-a
+          \global@ACM@balancefalse
+    \fi
+  \fi
+}
+\AtEndDocument{%
+  \if@ACM@balance
+  \if@twocolumn
+  \balance
+  \fi\fi}
+\newcommand\acksname{Acknowledgments}
+\specialcomment{acks}{%
+  \begingroup
+  \section*{\acksname}
+  \phantomsection\addcontentsline{toc}{section}{\acksname}
+}{%
+  \endgroup
+}
+\def\grantsponsor#1#2#3{#2}
+\newcommand\grantnum[3][]{#3%
+  \def@tempa{#1}\ifx@tempa@empty\else\space(\url{#1})\fi}
+\AtEndPreamble{%
+\if@ACM@screen
+  \includecomment{screenonly}
+  \excludecomment{printonly}
+\else
+  \excludecomment{screenonly}
+  \includecomment{printonly}
+\fi
+\if@ACM@anonymous
+  \excludecomment{anonsuppress}
+  \excludecomment{acks}
+\else
+  \includecomment{anonsuppress}
+\fi}
+\newcommand\showeprint[2][arxiv]{%
+  \def@tempa{#1}%
+  \ifx@tempa@empty\def@tempa{arxiv}\fi
+  \def@tempb{arxiv}%
+  \ifx@tempa@tempb
+     arXiv:\href{http://arxiv.org/abs/#2%7D%7B#2%7D%5Celse arXiv:#2%
+  \fi}
+\let@vspace@orig=@vspace
+\let@vspacer@orig=@vspacer
+\apptocmd{@vspace}{\ClassWarning{@classname}{\string\vspace\space should
+    only be used to provide space above/below surrounding
+    objects}}{}{}
+\apptocmd{@vspacer}{\ClassWarning{@classname}{\string\vspace\space should
+    only be used to provide space above/below surrounding
+    objects}}{}{}
+\let\ACM@origbaselinestretch\baselinestretch
+\AtEndDocument{\ifx\baselinestretch\ACM@origbaselinestretch\else
+  \ClassError{@classname}{An attempt to redefine
+    \string\baselinestretch\space detected.  Please do not do this for
+    ACM submissions!}\fi}
+\normalsize\normalfont\frenchspacing
+\endinput
+%%
+%% End of file `acmart.cls'.
=====================================
paper.tex
=====================================
The diff for this file was not included because it is too large.
=====================================
refs.bib
=====================================
@@ -1,12 +1,12 @@
-@techreport{Monnier19a,
+@inproceedings{Monnier19,
   author =        {Stefan Monnier},
+  booktitle =     {Journées Francophones des Langages Applicatifs},
   institution =   {Université de Montréal - DIRO},
+  pages =         {193-208},
   title =         {Typer: {ML} boosted with type theory and {S}cheme},
   year =          {2019},
-  url =           {https://www.iro.umontreal.ca/%5C~%7B%7Dmonnier/typer-overview-
-                  2019.pdf},
 }
@misc{Coq00,
@@ -18,32 +18,12 @@
   year =          {2000},
 }
-@inproceedings{Bove09,
-  author =        {Ana Bove and Peter Dybjer and Ulf Norell},
-  booktitle =     {International Conference on Theorem Proving in
-                   Higher-Order Logics},
-  key =           {TPHOLs09},
-  month =         aug,
-  pages =         {73-78},
-  series =        {Lecture Notes in Computer Science},
-  title =         {A Brief Overview of {A}gda – A Functional Language
-                   with Dependent Types},
-  volume =        {5674},
-  year =          {2009},
-  abstract =      {We give an overview of Agda, the latest in a series
-                   of dependently typed programming languages developed
-                   in Gothenburg. Agda is based on Martin-Löf’s
-                   intuitionistic type theory but extends it with
-                   numerous programming language features. It supports a
-                   wide range of inductive data types, including
-                   inductive families and inductive-recursive types,
-                   with associated flexible pattern-matching. Unlike
-                   other proof assistants, Agda is not tactic-based.
-                   Instead it has an Emacs-based interface which allows
-                   programming by gradual refinement of incomplete
-                   type-correct terms.},
-  url =           {http://www.cse.chalmers.se/%5C~%7B%7Dulfn/papers/tphols09/
-                  tutorial.pdf},
+@phdthesis{Norell07,
+  author =        {Ulf Norell},
+  school =        {Chalmers university},
+  title =         {Towards a Practical Programming Language Based on
+                   Dependent Type Theory},
+  year =          {2007},
 }
@article{Brady13,
@@ -74,7 +54,6 @@
                    Furthermore, I show how this method facilitates the
                    implementation of new high-level language
                    constructs.},
-  url =           {https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf%7D,
 }
@inproceedings{Swamy16,
@@ -132,7 +111,6 @@
                    combination of SMT automation and constructive
                    proofs, enabling a tactic-free style of programming
                    and proving at a relatively large scale.},
-  url =           {https://dl.acm.org/citation.cfm?id=2837655%7D,
 }
@inproceedings{Casinghino14,
@@ -165,7 +143,6 @@
                    programmers to work with total and partial functions
                    uniformly, providing a smooth path from functional
                    programming to dependently-typed programming.},
-  url =           {https://dl.acm.org/citation.cfm?id=2535883%7D,
 }
@inproceedings{Paulin93,
@@ -180,8 +157,6 @@
   title =         {Inductive definitions in the system {Coq}---rules and
                    properties},
   year =          {1993},
-  url =           {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR1992/RR1992-
-                  49.ps.Z},
 }
@techreport{Gimenez94,
@@ -211,8 +186,6 @@
                    different reduction rules from the ones used in [5]
                    in order to obtain a decidable conversion relation
                    for the system.},
-  url =           {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR1995/RR1995-
-                  07.ps.Z},
 }
@book{Milner97,
@@ -297,7 +270,6 @@
                    systems. In that way the well-known
                    propositions-as-types interpretation obtains a nice
                    canonical form.},
-  url =           {http://www.jeremyherve.net/bar91.pdf%7D,
 }
@inproceedings{Luo89,
@@ -309,6 +281,29 @@
   year =          {1989},
 }
+@inproceedings{Sulzmann07,
+  address =       {Nice, France},
+  author =        {Martin Sulzmann and Manuel M. T. Chakravarty and
+                   Simon {Peyton Jones} and Kevin Donnelly},
+  booktitle =     {Types in Language Design and Implementation},
+  key =           {{TLDI}'07},
+  month =         jan,
+  pages =         {53-66},
+  title =         {System F with Type Equality Coercions},
+  year =          {2007},
+  abstract =      {We introduce System F_C , which extends System F with
+                   support for non-syntactic type equality. There are
+                   two main extensions: (i) explicit witnesses for type
+                   equalities, and (ii) open, non-parametric type
+                   functions, given meaning by top-level equality
+                   axioms. Unlike System F, F_C is expressive enough to
+                   serve as a target for several different
+                   source-language features, including Haskell's
+                   newtype, generalised algebraic data types, associated
+                   types, functional dependencies, and perhaps more
+                   besides.},
+}
+
 @inproceedings{Coquand92,
   author =        {Thierry Coquand},
   booktitle =     {Workshop on Types for Proofs and Programs},
@@ -317,6 +312,132 @@
   year =          {1992},
 }
+@inproceedings{Miquel01,
+  author =        {Alexandre Miquel},
+  booktitle =     {International conference on Typed Lambda Calculi and
+                   Applications},
+  key =           {TLCA'01},
+  pages =         {344-359},
+  title =         {The implicit calculus of constructions: extending
+                   pure type systems with an intersection type binder
+                   and subtyping},
+  year =          {2001},
+  abstract =      {In this paper, we introduce a new type system, the
+                   Implicit Calculus of Constructions, which is a
+                   Curry-style variant of the Calculus of Constructions
+                   that we extend by adding an intersection type
+                   binder-called the implicit dependent product. Unlike
+                   the usual approach of Type Assignment Systems, the
+                   implicit product can be used at every place in the
+                   universe hierarchy. We study syntactical properties
+                   of this calculus such as the βη-subject reduction
+                   property, and we show that the implicit product
+                   induces a rich subtyping relation over the type
+                   system in a natural way. We also illustrate the
+                   specificities of this calculus by revisiting the
+                   impredicative encodings of the Calculus of
+                   Constructions, and we show that their translation
+                   into the implicit calculus helps to reflect the
+                   computational meaning of the underlying terms in a
+                   more accurate way.},
+}
+
+@inproceedings{Barras08,
+  address =       {Budapest, Hungary},
+  author =        {Bruno Barras and Bruno Bernardo},
+  booktitle =     {Conference on Foundations of Software Science and
+                   Computation Structures},
+  month =         apr,
+  series =        {Lecture Notes in Computer Science},
+  title =         {Implicit Calculus of Constructions as a Programming
+                   Language with Dependent Types},
+  volume =        {4962},
+  year =          {2008},
+  abstract =      {In this paper, we show how Miquel’s Implicit
+                   Calculus of Constructions (ICC) can be used as a
+                   programming language featuring dependent types. Since
+                   this system has an undecidable type-checking, we
+                   introduce a more verbose variant, called ICC∗ which
+                   fixes this issue. Datatypes and program
+                   specifications are enriched with logical assertions
+                   (such as preconditions, postconditions, invariants)
+                   and programs are decorated with proofs of those
+                   assertions. The point of using ICC∗ rather than the
+                   Calculus of Constructions (the core formalism of the
+                   Coq proof assistant) is that all of the static
+                   information (types and proof objects) is transparent,
+                   in the sense that it does not affect the
+                   computational behavior. This is concretized by a
+                   built-in extraction procedure that removes this
+                   static information. We also illustrate the main
+                   features of ICC∗ on classical examples of
+                   dependently typed programs.},
+}
+
+@inproceedings{MishraLinger08,
+  address =       {Budapest, Hungary},
+  author =        {Nathan Mishra-Linger and Tim Sheard},
+  booktitle =     {Conference on Foundations of Software Science and
+                   Computation Structures},
+  month =         apr,
+  pages =         {350-364},
+  series =        {Lecture Notes in Computer Science},
+  title =         {Erasure and Polymorphism in Pure Type Systems},
+  volume =        {4962},
+  year =          {2008},
+  abstract =      {We introduce Erasure Pure Type Systems, an extension
+                   to Pure Type Systems with an erasure semantics
+                   centered around a type constructor indicating
+                   parametric polymorphism. The erasure phase is guided
+                   by lightweight program annotations. The typing rules
+                   guarantee that well-typed programs obey a phase
+                   distinction between erasable (compile-time) and
+                   non-erasable (run-time) terms. The erasability of an
+                   expression depends only on how its value is used in
+                   the rest of the program. Despite this simple
+                   observation, most languages treat erasability as an
+                   intrinsic property of expressions, leading to code
+                   duplication problems. Our approach overcomes this
+                   deficiency by treating erasability extrinsically.
+                   Because the execution model of EPTS generalizes the
+                   familiar notions of type erasure and parametric
+                   polymorphism, we believe functional programmers will
+                   find it quite natural to program in such a setting.},
+}
+
+@inproceedings{Castagna16,
+  author =        {Giuseppe Castagna and Tommaso Petrucciani and
+                   Kim Nguyên},
+  booktitle =     {International Conference on Functional Programming},
+  key =           {ICFP'16},
+  month =         sep,
+  pages =         {378-391},
+  title =         {Set-theoretic types for polymorphic variants},
+  year =          {2016},
+  abstract =      {Polymorphic variants are a useful feature of the
+                   OCaml language whose current definition and
+                   implementation rely on kinding constraints to
+                   simulate a subtyping relation via unification. This
+                   yields an awkward formalization and results in a type
+                   system whose behaviour is in some cases unintuitive
+                   and/or unduly restrictive. In this work, we present
+                   an alternative formalization of polymorphic variants,
+                   based on set-theoretic types and subtyping, that
+                   yields a cleaner and more streamlined system. Our
+                   formalization is more expressive than the current one
+                   (it types more programs while preserving type
+                   safety), it can internalize some meta-theoretic
+                   properties, and it removes some pathological cases of
+                   the current implementation resulting in a more
+                   intuitive and, thus, predictable type system. More
+                   generally, this work shows how to add full-fledged
+                   union types to functional languages of the ML family
+                   that usually rely on the Hindley-Milner type system.
+                   As an aside, our system also improves the theory of
+                   semantic subtyping, notably by proving completeness
+                   for the type reconstruction algorithm.},
+}
+
 @inproceedings{Blume06,
   address =       {Portland, Oregon},
   author =        {Matthias Blume and Umut A. Acar and Wonseok Chae},
@@ -353,47 +474,57 @@
                    (currently for PowerPC) and optimizes the
                    representation of sums by eliminating closures
                    generated by the dual construction.},
-  url =           {https://dl.acm.org/citation.cfm?id=1159836%7D,
 }
-@inproceedings{Castagna16,
-  author =        {Giuseppe Castagna and Tommaso Petrucciani and
-                   Kim Nguyên},
-  booktitle =     {International Conference on Functional Programming},
-  key =           {ICFP'16},
+@inproceedings{Monnier07,
+  address =       {Freiburg, Germany},
+  author =        {Stefan Monnier},
+  booktitle =     {Programming Languages meets Program Verification},
+  key =           {PLPV'07},
   month =         sep,
-  pages =         {378-391},
-  title =         {Set-theoretic types for polymorphic variants},
-  year =          {2016},
-  abstract =      {Polymorphic variants are a useful feature of the
-                   OCaml language whose current definition and
-                   implementation rely on kinding constraints to
-                   simulate a subtyping relation via unification. This
-                   yields an awkward formalization and results in a type
-                   system whose behaviour is in some cases unintuitive
-                   and/or unduly restrictive. In this work, we present
-                   an alternative formalization of polymorphic variants,
-                   based on set-theoretic types and subtyping, that
-                   yields a cleaner and more streamlined system. Our
-                   formalization is more expressive than the current one
-                   (it types more programs while preserving type
-                   safety), it can internalize some meta-theoretic
-                   properties, and it removes some pathological cases of
-                   the current implementation resulting in a more
-                   intuitive and, thus, predictable type system. More
-                   generally, this work shows how to add full-fledged
-                   union types to functional languages of the ML family
-                   that usually rely on the Hindley-Milner type system.
-                   As an aside, our system also improves the theory of
-                   semantic subtyping, notably by proving completeness
-                   for the type reconstruction algorithm.},
-  url =           {https://dl.acm.org/citation.cfm?id=2951928%7D,
+  pages =         {33-40},
+  publisher =     {ACM Press},
+  title =         {The {S}wiss Coercion},
+  year =          {2007},
+  abstract =      {Recent type systems allow the programmer to use types
+                   that describe more precisely the invariants on which
+                   the program relies. But in order to satisfy the type
+                   system, it often becomes necessary to help the type
+                   checker with extra annotations that justify why a
+                   piece of code is indeed well-formed. Such annotations
+                   take the form of term-level type manipulations, such
+                   as type abstractions, type applications, existential
+                   package packing and opening, as well as
+                   \emph{coercions}, or \emph{casts}. While those
+                   operations have no direct runtime cost, they tend to
+                   introduce extra runtime operations equivalent to
+                   $\eta$-redexes or even empty loops in order to get to
+                   the point where we can apply that supposedly free
+                   operation. We show a coercion that is like a pacific
+                   Swiss army knife of coercions: it cannot cut but it
+                   can instantiate, open, pack, abstract, analyze, or do
+                   any combination thereof, reducing the need for extra
+                   surrounding runtime operations. And all that, of
+                   course, for the price of a single coercion, which
+                   still costs absolutely nothing at runtime. This new
+                   coercion is derived from Karl Crary's coercion
+                   calculus~\cite{Crary00}, but can also replace Crary
+                   and Weirich's \kw{vcase}~\cite{Weirich99}. It
+                   additionally happens to come in handy to work around
+                   some limitations of value polymorphism. It is
+                   presented in the context of Shao et al.'s Type System
+                   for Certified Binaries~\cite{Shao02}. Other than the
+                   coercion itself, another interesting aspect of this
+                   work is a slightly unusual proof technique to show
+                   soundness of the type erasure using a pure type
+                   assignment language, making the no-op nature of our
+                   \kw{cast} more obvious.},
 }
@inproceedings{Chapman10,
   address =       {Baltimore, MD},
   author =        {James Chapman and Pierre-{'E}variste Dagand and
-                   Connor McBride and Peter Morris},
+                   Conor McBride and Peter Morris},
   booktitle =     {International Conference on Functional Programming},
   key =           {ICFP'10},
   month =         sep,
@@ -416,59 +547,21 @@
                    or infinite regress.},
 }
-@inproceedings{Christiansen16,
-  author =        {David Christiansen and Edwin Brady},
-  booktitle =     {International Conference on Functional Programming},
-  key =           {ICFP'16},
-  month =         sep,
-  pages =         {284-297},
-  title =         {Elaborator Reflection: Extending {I}dris in {I}dris},
-  year =          {2016},
-  abstract =      {Many programming languages and proof assistants are
-                   defined by elaboration from a high-level language
-                   with a great deal of implicit information to a highly
-                   explicit core language. In many advanced languages,
-                   these elaboration facilities contain powerful tools
-                   for program construction, but these tools are rarely
-                   designed to be repurposed by users. We describe
-                   elaborator reflection, a paradigm for metaprogramming
-                   in which the elaboration machinery is made directly
-                   available to metaprograms, as well as a concrete
-                   realization of elaborator reflection in Idris, a
-                   functional language with full dependent types. We
-                   demonstrate the applicability of Idris’s reflected
-                   elaboration framework to a number of realistic
-                   problems, we discuss the motivation for the specific
-                   features of its design, and we explore the broader
-                   meaning of elaborator reflection as it can relate to
-                   other languages.},
-  url =           {https://eb.host.cs.st-andrews.ac.uk/drafts/elab-
-                  reflection.pdf},
-}
-
-@inproceedings{Firsov18,
-  author =        {Denis Firsov and Aaron Stump},
-  booktitle =     {Certified Programs and Proofs},
-  pages =         {215-227},
-  title =         {Generic Derivation of Induction for Impredicative
-                   Encodings in Cedille},
-  year =          {2018},
-  abstract =      {This paper presents generic derivations of induction
-                   for impredicatively typed lambda-encoded datatypes,
-                   in the Cedille type theory. Cedille is a pure type
-                   theory extending the Curry-style Calculus of
-                   Constructions with implicit products, primitive
-                   heterogeneous equality, and dependent intersections.
-                   All data erase to pure lambda terms, and there is no
-                   built-in notion of datatype. The derivations are
-                   generic in the sense that we derive induction for any
-                   datatype which arises as the least fixed point of a
-                   signature functor. We consider Church-style and
-                   Mendler-style lambda-encodings. Moreover, the
-                   isomorphism of these encodings is proved. Also, we
-                   formalize Lambek's lemma as a consequence of expected
-                   laws of cancellation, reflection, and fusion.},
-  url =           {http://doi.acm.org/10.1145/3167087%7D,
+@inproceedings{Odersky97,
+  author =        {Martin Odersky and Philip Wadler},
+  booktitle =     {Symposium on Principles of Programming Languages},
+  key =           {POPL'97},
+  month =         jan,
+  title =         {Pizza into Java: Translating Theory into Practice},
+  year =          {1997},
+  abstract =      {Pizza is a strict superset of Java that incorporates
+                   three ideas from the academic community: parametric
+                   polymorphism, higher-order functions, and algebraic
+                   data types. Pizza is defined by translation into Java
+                   and compiles into the Java Virtual Machine,
+                   requirements which strongly constrain the design
+                   space. Nonetheless, Pizza fits smoothly to Java, with
+                   only a few rough edges.},
 }
@inproceedings{Altenkirch10,
@@ -501,7 +594,30 @@
                    translating several high-level constructions, that
                    ΠΣ is suitable as a core language for dependently
                    typed programming.},
-  url =           {http://www.cs.nott.ac.uk/%5C~%7B%7Dpsztxa/publ/pisigma-new.pdf%7D,
+}
+
+@inproceedings{Firsov18,
+  author =        {Denis Firsov and Aaron Stump},
+  booktitle =     {Certified Programs and Proofs},
+  pages =         {215-227},
+  title =         {Generic Derivation of Induction for Impredicative
+                   Encodings in Cedille},
+  year =          {2018},
+  abstract =      {This paper presents generic derivations of induction
+                   for impredicatively typed lambda-encoded datatypes,
+                   in the Cedille type theory. Cedille is a pure type
+                   theory extending the Curry-style Calculus of
+                   Constructions with implicit products, primitive
+                   heterogeneous equality, and dependent intersections.
+                   All data erase to pure lambda terms, and there is no
+                   built-in notion of datatype. The derivations are
+                   generic in the sense that we derive induction for any
+                   datatype which arises as the least fixed point of a
+                   signature functor. We consider Church-style and
+                   Mendler-style lambda-encodings. Moreover, the
+                   isomorphism of these encodings is proved. Also, we
+                   formalize Lambek's lemma as a consequence of expected
+                   laws of cancellation, reflection, and fusion.},
 }
@proceedings{FLOPS10,
@@ -513,6 +629,18 @@
   year =          {2010},
 }
+@proceedings{FOSSACS08,
+  address =       {Budapest, Hungary},
+  booktitle =     {Conference on Foundations of Software Science and
+                   Computation Structures},
+  month =         apr,
+  series =        {Lecture Notes in Computer Science},
+  title =         {Conference on Foundations of Software Science and
+                   Computation Structures},
+  volume =        {4962},
+  year =          {2008},
+}
+
 @proceedings{ICFP06,
   address =       {Portland, Oregon},
   booktitle =     {International Conference on Functional Programming},
@@ -522,18 +650,6 @@
   year =          {2006},
 }
-@proceedings{TPHOLs09,
-  booktitle =     {International Conference on Theorem Proving in
-                   Higher-Order Logics},
-  key =           {TPHOLs09},
-  month =         aug,
-  series =        {Lecture Notes in Computer Science},
-  title =         {International Conference on Theorem Proving in
-                   Higher-Order Logics},
-  volume =        {5674},
-  year =          {2009},
-}
-
 @proceedings{POPL14,
   booktitle =     {Symposium on Principles of Programming Languages},
   key =           {POPL'14},
@@ -594,6 +710,33 @@
   year =          {1989},
 }
+@proceedings{TLCA01,
+  booktitle =     {International conference on Typed Lambda Calculi and
+                   Applications},
+  key =           {TLCA'01},
+  title =         {International conference on Typed Lambda Calculi and
+                   Applications},
+  year =          {2001},
+}
+
+@proceedings{PLPV07,
+  address =       {Freiburg, Germany},
+  booktitle =     {Programming Languages meets Program Verification},
+  key =           {PLPV'07},
+  month =         sep,
+  publisher =     {ACM Press},
+  title =         {Programming Languages meets Program Verification},
+  year =          {2007},
+}
+
+@proceedings{POPL97,
+  booktitle =     {Symposium on Principles of Programming Languages},
+  key =           {POPL'97},
+  month =         jan,
+  title =         {Symposium on Principles of Programming Languages},
+  year =          {1997},
+}
+
 @proceedings{TLCA93,
   booktitle =     {International conference on Typed Lambda Calculi and
                    Applications},
@@ -615,6 +758,15 @@
   year =          {1997},
 }
+@proceedings{TLDI07,
+  address =       {Nice, France},
+  booktitle =     {Types in Language Design and Implementation},
+  key =           {{TLDI}'07},
+  month =         jan,
+  title =         {Types in Language Design and Implementation},
+  year =          {2007},
+}
+
 @proceedings{POPL16,
   booktitle =     {Symposium on Principles of Programming Languages},
   key =           {POPL'16},
=====================================
slides.tex
=====================================
@@ -0,0 +1,614 @@
+\documentclass[display,semhelv]{seminar}
+%% \documentclass{slides}
+
+\newcommand \CourseName {~~~~~~~~CUC}
+\input{../../myslides}
+\usepackage{mathpartir}
+\usepackage{amsthm}
+
+\newtheorem{theorem}{Theorem}[section]
+\newtheorem{lemma}[theorem]{Lemma}
+
+\newcommand \Subst[3] {#1[#2/#3]}
+
+\newcommand \Infer[1][] {\inferrule*[right=#1]}
+\newcommand \Rname[1] {#1}
+
+\newcommand \Ferase[1] {{#1*}}
+\newcommand \Fforget[1] {\lfloor#1\rfloor}
+
+\newcommand \Jtype[2][\Gamma] {#1 \vdash #2~:~}
+\newcommand \Jcic \Jtype
+\newcommand \Jcon[2][x;y] {#1 \vdash #2;;\kw{con}}
+\newcommand \Jsmall[2][\Gamma] {#1 \vdash #2;;\kw{small}}
+
+\newcommand \Type[1] {\kw{Type}_{#1}}
+\newcommand \Tmax[1] {#1~\sqcup~}
+
+\newcommand \TEarw[1][\ensuremath{k}] {\stackrel{\kw{#1}}{\to}}
+\newcommand \TEapp[2][\ensuremath{k}] {#2@^{\kw{#1}}}
+
+\newcommand \Lam[3][\ensuremath{k}] {\lambda #2 : #3 \TEarw[#1]}
+\newcommand \Arw[3][\ensuremath{k}] {(#2 : #3) \TEarw[#1]}
+\newcommand \ArwS[2][\ensuremath{k}] {#2 \TEarw[#1]}
+\newcommand \App \TEapp
+
+\newcommand \Ind[3] {\kw{Ind}(#1:#2)\langle#3\rangle}
+\newcommand \Con[2] {\kw{Con}(#1,#2)}
+\newcommand \Case[3] {\langle#1\rangle\kw{Case}~#2 ~\kw{of}~\langle#3\rangle}
+\newcommand \Fix[3] {\kw{Fix}_{#1}~#2:#3~=~}
+\newcommand \ArwM[3][\ensuremath{k}] {\overrightarrow{(#2:#3)\TEarw[#1]},}
+\newcommand \LamM[3][\ensuremath{k}] {\lambda\overrightarrow{#2:#3\TEarw[#1]},}
+\newcommand \AppM[3][\ensuremath{k}] {#2~\overrightarrow{\TEapp[#1]{}#3}}
+
+\newcommand \IndE[2] {\kw{Ind}(#1)\langle#2\rangle}
+\newcommand \ConE[1] {\kw{Con}(#1)}
+\newcommand \CaseE[2] {\kw{Case}~#1 ~\kw{of}~\langle#2\rangle}
+\newcommand \FixE[1] {\kw{Fix}~#1~=~}
+
+\begin{document}
+
+\renewcommand \thepagetail {/87\hspace{-5pt}}
+
+\begin{myslide}{}               %Title page
+
+  \begin{center}
+    \vfill
+
+    {\huge
+     Inductive Types Deconstructed \medskip \
+     The Calculus of \smallskip \ United Constructions
+    }
+
+    \vfill \vfill
+
+    Stefan Monnier \ \texttt{monnier@iro.umontreal.ca} \
+    Université de Montréal
+
+    \vfill
+  \end{center}
+
+\end{myslide}
+
+\renewcommand \righthead {Introduction}
+
+\renewcommand{\CancelColor}{\color{red}}
+
+%% - Inductive/data types: big and bloated.
+%% - Inefficient projection from tuples.
+%% - Impossibility to project separately from a case-test.
+%% - why not do it like SML?
+%% - No type refinement in default branches.
+%% - Done here for CIC but usable elsewhere
+%% - Give a bit of Typer context (can't throw away types yet!)
+%%
+%% - Decomposition into: tuples, unions, recursion, equality
+%% - tagged tuples
+%% - equality
+%% - unions
+%%   boolean blindness
+%% - recursion
+%% - erasure
+%% - consistency
+
+%% Union themes:
+%% - wage
+%% - grievance procedure
+%% - representation
+%% - union organizer
+%% - rights!
+%% - right to organize
+%% - bargaining power
+%% - negotiation
+%% - contract negotiation
+%% - go on strike
+%% - lockout
+%% - labor dispute
+%% - capital
+%% - exploitation
+%% - unfair labor practice
+%% - scab
+
+\begin{myslide}{Inductive types}
+  \hfill Inductive types \hfill||\hfill GADTs \hfill||\hfill Datatypes
+  \hfill\mbox{}
+
+  \vfill
+
+  \SMCenterLine{Swiss army knives of data types:}
+
+  \SMCenterLine{Sum types + Product types (+ Recursive types + Indexed types)}
+
+  \vfill
+
+  Love/hate relationship:
+  \begin{itemize}
+  \item[${+}$] Handy packaging of all those constructs
+  \item[${-}$] Big and bulky: can't always fit in my pockets
+  \end{itemize}
+
+  \vfill
+  %% \SMCenterLine{The calculus of United Constructions}
+  \SMCenterLine{¡ Here's how to break them {down into their constituents }!}
+\end{myslide}
+
+\newcommand \RedStep [1] {%
+  \switch[][\boolean{firstactivation}]{#1}{{\color{red}{#1}}}%
+}
+\newcommand \RedReStep [2] {%
+  \reswitch[\value{step}=#1][\boolean{firstactivation}]{#2}{{\color{red}{#2}}}%
+}
+
+\begin{myslide}{Sample definition}
+  %% \vfill
+  \stepwise{
+    \vspace{-15pt}
+    %% \vfill
+    \begin{displaymath}
+      \MAlign{
+        \kw{type}~~\id{NList}~\RedReStep 5 \alpha~\RedReStep 4 n \[-3pt]
+        ~~\begin{array}{l@{~}l@{~}l}
+          \mid \id{\RedReStep 1 {nil}} &
+              : &
+              \id{NList}~\RedReStep 5 \alpha~\RedReStep 4 0 \[-3pt]
+          \mid \id{\RedReStep 1 {cons}} &
+              : \RedReStep 2 {\alpha} \to \RedReStep 2 {\id{\RedReStep 3 {NList}}~\RedReStep
+            5 \alpha~\RedReStep 4{n'}} \to & \id{NList}~\RedReStep 5 \alpha~\RedReStep 4{(S~n')}
+        \end{array}
+      }
+    \end{displaymath}
+    \vfill
+    %%
+    Canonical example using all the features:
+    \vfill
+    \begin{center}
+      \begin{tabular}{cl}
+        \texttt{\RedStep {nil | cons}} &
+            Sum type \
+        \texttt{\RedStep {cons~x~xs}} & Product type \
+        \texttt{\RedStep {NList}} & Recursive type \
+        $\color{black}\RedStep{n}$ & Indexed type \
+        $\color{black}\RedStep{\alpha}$ & Parameterized type \
+      \end{tabular}
+    \end{center}
+    \RedStep {} %FIXME: For some reason, the last step is skipped otherwise!
+    \vfill      %Helps vertical alignment!
+  }
+\end{myslide}
+
+\begin{myslide}{Sample use}
+  \stepwise{
+    %% \vspace{-10pt}
+    %% \switch[\value{step}=3]{\mbox{}%% \newline
+    %%                         \mbox{}}{}
+    Constructors and destructors:
+    {\small
+      \begin{displaymath}
+        \MAlign{
+          \id{map} : (?\alpha \to~?\beta) \to \id{NList}~~?\alpha~~\RedReStep 4 {?n}
+          \to \id{NList}~~?\beta~~\RedReStep 4 {?n}; \[-3pt]
+          \id{map}~~f~~xs = \kw{case}~~\RedReStep 3 {xs}  \[-3pt]
+          ~~\begin{array}{l@{~}l}
+            \mid \id{\RedReStep 1 {cons}}~~\RedReStep 2 {y~~ys} &
+            \Rightarrow \id{cons}~(f~y)~(\id{map}~f~ys)  \[-3pt]
+            \mid \id{\RedReStep 1 {_}} & \Rightarrow \id{nil}
+          \end{array}
+        }
+      \end{displaymath}}
+    %% \begin{center}
+    %%   \begin{tabular}{ll}
+    %%     \texttt{cons (f x) (map f xs)} & Constructor \
+    %%     \texttt{nil} & Constructor \
+    %%     \texttt{case} & \TAlign{Does-it-all Destructor!}
+    %%   \end{tabular}
+    %% \end{center}
+    %%
+    \texttt{case} destructor does it all:
+    \vfill
+    \begin{itemize}
+    \item \RedStep{Select} the right branch (Sum type)
+    \item \RedStep{Extract} the fields (Product type)
+    \item \RedStep{Unfold} the type (Recursive type)
+    \item \RedStep{Refine} the type within branches (Indexed type)
+    \end{itemize}
+    \vfill      %Helps vertical alignment!
+  }
+\end{myslide}
+
+\renewcommand \righthead {Apertizer}
+
+\begin{myslide}{Grievances from Product types}
+  Extraction of a single tuple field
+  \hfill$\Rightarrow$\hfill \kw{case} expression of size $\color{black}O(N)$
+  %%
+  \begin{displaymath}
+    x.1 ~~~~~⇒~~~~~
+    \texttt{case}~~x~~|~~\texttt{tuple}~x_1~x_2~...~x_n\texttt{~=>~}x_1
+  \end{displaymath}
+
+  Can't extract fields separately from a constructor test
+  \begin{displaymath}
+    \MAlign{\texttt{case}~~x \
+            ~~|~\texttt{cons}~_~_\texttt{~=>~}
+            ~...~
+            \MAlign{\texttt{case}~~x \
+                    ~~|~\texttt{cons}~~y~~ys\texttt{~=>~} ... \
+                    ~~|~~?\texttt{~=>~}?
+            }
+    }
+  \end{displaymath}
+  Fine for high-level language, limiting for low-level language
+\end{myslide}
+
+\begin{myslide}{First rejected offer}
+  \SMCenterLine{¿ Promise to increase the wage of the optimizer ?}
+
+  \begin{itemize}
+  \item Live with suboptimal source code
+  \item Hope later optimization phases will generate the better code
+  \end{itemize}
+
+  \vfill \pause \vfill
+
+  \SMCenterLine{¡ Not good enough !}
+
+  Working on Typer, an ML/Haskell with dependent types and macros
+
+  We need to type check the lower-level code:
+
+  \SMCenterLine{We want to implement such optimizations via metaprogramming}
+\end{myslide}
+
+\begin{myslide}{Second rejected offer}
+  %% \SMCenterLine{¿ Do it like Standard ML ?}
+  \SMCenterLine{¿ Standard ML:~~tuples + disjoint sums ?}
+  \begin{itemize}
+  \item Each datatype constructor takes exactly one argument
+  \item Add separate Tuple types
+  \end{itemize}
+  
+  \vfill\pause\vfill
+
+  \SMCenterLine{¡ Not good enough !}
+
+  Now $\id{cons}(x,y)$ uses up 2 heap objects:
+  
+  \begin{center}
+    \begin{picture}(200,15)
+      \put(30,0){\fbox{$~\id{cons}~$ ${\color{black}\mid}$ \hspace{3em}}}
+      \put(130,0){\fbox{${~~~~x~~~~}$ ${\color{black}\mid}$ ${~~~~y~~~~}$}}
+      \thicklines
+      \put(75,3){\vector(1,0){50}}
+    \end{picture}
+  \end{center}
+  \vfill
+
+  %% \SMCenterLine
+  {Don't want to rely on optimizer to merge them back (see 1st offer)}
+\end{myslide}
+
+\begin{myslide}{Grievances from Sum types}
+  {\small
+    \begin{displaymath}
+      \MAlign{
+        \id{map} : (?\alpha \to~?\beta) \to \id{NList}~~?\alpha~~?n \to \id{NList}~~?\beta~~?n; \[-3pt]
+        \id{map}~~f~~xs = \kw{case}~~xs  \[-3pt]
+        ~~
+        \begin{array}{l@{~}l}
+          \mid \id{cons}~~y~~ys & \Rightarrow \id{cons}~(f~y)~(\id{map}~f~ys)  \[-3pt]
+          \mid _ & \Rightarrow \id{nil}
+        \end{array}
+      }
+    \end{displaymath}
+  }
+  \vfill
+  \SMCenterLine{¡ doesn't type check !}
+  \vfill
+  \vfill
+  
+  \SMCenterLine{
+    The default branch does not know that $xs$ is $\id{nil}$}
+  \vfill
+\end{myslide}
+
+%% FIXME!!
+%% \begin{myslide}{The case for unionization}
+%%   Inductive types alienate the constructs they employ
+%%
+%%   Sum, Product, Recursive, and Indexed types deserve more respect
+%%
+%%   End the oppression of inductive types
+%%
+%%   Let its constituents negotiate their own contract
+%% \end{myslide}
+
+\renewcommand \righthead {Main dish}
+
+\begin{myslide}{The Calculus of United Constructions (CUC)}
+  Lower-level definition for the Calculus of Inductive Constructions (CIC)
+
+  Deconstruct inductive types into:
+  \begin{center}
+    \begin{tabular}{l@{~~⇒~~}l}
+      Product types & \emph{Labeled} tuples \
+      Sum types & \emph{Non-disjoint} union types \
+      Recursion & Good old ${\color{black}\mu}$-types \
+      Indexed typed & Equality types \
+    \end{tabular}
+
+    \vfill
+    ¡ Put the labels on the products rather than the sums !
+
+    Same approach applicable to other settings, e.g.\ GADTs, datatypes
+  \end{center}
+\end{myslide}
+
+\newcommand \EmptyCtx {\bullet}
+\newcommand \Ttagvar {l}
+\newcommand \Tuple[2][\Ttagvar] {\kw{Tuple}_{#1}~#2}
+\newcommand \tuple[2][\Ttagvar] {\kw{tuple}_{#1}~}%% ~{#2}
+%% \newcommand \tuple[3][\Ttagvar] {{ #3 : #2 }_{#1}}
+\newcommand \TLabel {\id{Label}}
+\newcommand \Let[2] {\kw{let}~#1 = #2~\kw{in}~}
+\newcommand \Tproj[1] {#1.}
+
+\begin{myslide}{Labeled tuples}
+  \vspace{-10pt}
+  %%
+  {\small \begin{displaymath}
+    \color{mathgreen}
+    \texttt{cons 7 nil}
+    ~~{\color{black}\Rightarrow}~~
+    \tuple[\color{red}\textsf{cons}] \Delta {(7,\texttt{nil})}
+    ~~{\color{black}:}~~
+    \Tuple[\color{red}\textsf{cons}]
+          {(\textsf{Int}, \texttt{NList}~\textsf{Int}~0)}
+  \end{displaymath}}
+  Good Old Tuples Types™ plus label annotation and dependent types
+  %%
+  \begin{displaymath}
+    %% \begin{array}{l@{;:;}l}
+    %%   \TLabel & \Type 0; \
+    %%   `Tcons Int Tnil : Types 0` comparable to `cons Int nil : list Type₀`
+    %%   `list Int : Type₀` and `list Type₀ : Type₁` so `Types 0 : Type₁`!
+    %%   \id{Types}_\ell & \Type {\ell+1}; \
+    %%   \id{Tnil}_\ell & \id{Types}_\ell; \
+    %%   \id{Tcons} &
+    %%       \MAlign{\Tarw{t}{\Type{\ell_1}}
+    %%               {\Tsarw{(\Tsarw{t}{\id{Types}_{\ell_2}})}
+    %%                 {}} \
+    %%               ;;\id{Types}_{(\Tmax{\ell_1}{\ell_2});}} \medskip \
+    %%   \id{Values}_\ell & \Tsarw{\id{Types}_\ell}{\Type {\ell}}; \
+    %%   \id{Vnil}_\ell & \id{Values}_\ell~{\id{Tnil}_\ell}; \
+    %%   \id{Vcons}_\ell &
+    %%       \MAlign{
+    %%         \Tarw{x}{\tau}{\Tsarw{\id{Values}_\ell~{(f~x)}}{}} \
+    %%         ;; \id{Values}_\ell~{(\id{Tcons}~\tau~f)};
+    %%       } \medskip \
+    %%   \Tuple[]{} & \TLabel \to \id{Types}_\ell \to \Type \ell; \
+    %% \end{array}
+    \begin{array}{lc@{;;}c@{;;}l@{}}
+      %% \textsl{(label)} & l &\in& \mathcal{L} \
+      %% \textsl{(index)} & i &\in& \mathbb{N} \
+      \textsl{(ctxt)} & \Delta &::=& \EmptyCtx ~|~ \Delta,x:\tau \
+      \textsl{(term)} & e,\tau &::=&
+          ... \MAlign{~|~ \Tuple[{\color{red}\Ttagvar}] \Delta
+        ~|~ \tuple[{\color{red}\Ttagvar}] \Delta {\vec e} 
+        %% ~|~ \Tproj e i
+        ~|~ {\Let {\vec x} {e_1} {e_2}}} \
+      \textsl{(sugar)} & {\Tproj e i} &\equiv& \Let {\vec x} {e} {x_i}
+    \end{array}
+  \end{displaymath}
+  Labels on tuples are cheap
+  %% FIXME: BiBoP
+  \begin{itemize}
+  \item Can often be stashed in a pre-existing heap object header
+  \item At worst, adds a single word to heap objects (or use BiBoP)
+  \end{itemize}
+\end{myslide}
+
+\newcommand \Teq[1] {#1 \equiv}
+\newcommand \Trefl {\kw{refl}~}
+\newcommand \TJ[2] {\kw{J}~#1~#2~}
+
+\begin{myslide}{Equality type}
+  (Labeled) Tuples let us build \emph{non-indexed} single constructor types
+
+  To support \emph{indexing}, CUC provides an Equality type:
+  \begin{displaymath}
+    \begin{array}{lc@{;;}c@{;;}l}
+      \textsl{(term)} & e,\tau &::=&
+          ... ~|~ \Teq{e_1}{e_2} ~|~ \Trefl{e} ~|~ \TJ{e_\equiv}{e_f}{e}
+    \end{array}
+  \end{displaymath}
+
+  \texttt{NList} can be (re)defined without indexing:
+  \vspace{-5pt}
+  \begin{displaymath}
+    \MAlign{\kw{type}~~\id{NList}~\alpha~n \[-3pt]
+            ~~
+            \begin{array}{ll@{~~}l}
+              \mid & \id{nil} & (n \equiv 0) \[-3pt]
+              \mid &\id{cons} & \alpha~~(\id{NList}~\alpha~n')~~(n \equiv S~n')
+            \end{array}
+    }
+  \end{displaymath}
+  So \texttt{nil} returns $\tuple[\textsl{nil}]{Δ}{(\Trefl 0)}$
+
+  Saves us from the \emph{convoy pattern}
+  %%
+  and
+  %% Eliminates the need for
+  Coq's
+  $\color{mathgreen}\texttt{in}~\tau_1~\texttt{return}~\tau_2$
+  %% in \texttt{case}
+\end{myslide}
+
+\newcommand \TUnion[1] {#1~\cup~}
+\newcommand \TUnionSmart[1] {#1~\cup'~}
+%% Note: The first arg is not needed for type-checking, but it is
+%% needed for the reduction rules (so a cast from \tau to \tau can be dropped).
+\newcommand \TUcast[2] {\kw{cast}~#1{\subseteq}#2~}
+\newcommand \TUcase[6] {
+  \kw{switch}~#1~|~#2~#3~#3_\equiv\Rightarrow #4~|~#5~#5_\equiv\Rightarrow #6}
+
+\begin{myslide}{Non-disjoint union types}
+  Using labeled tuples and union types, we can (re)define \texttt{NList}:
+  \begin{displaymath}
+    \MAlign{
+      \kw{type}~\id{NList}~\alpha~n \
+      ~~=~\MAlign{
+        \Tuple[\textsl{nil}]{(\Teq{n}{0})} \
+        \cup~\Tuple[\textsl{cons}]{(n' : \textsl{Nat}, \alpha, \id{NList}~\alpha~n', \Teq{n}{S~n'})}
+      }
+    }
+    %% = (tuple)
+    %% | nil  (n ≡ 0)
+    %% | cons α (NList α n') (n ≡ S n'}
+  \end{displaymath}
+  \SMCenterLine{¡ Union types have no run-time representation/cost !}
+
+  But \texttt{nil}'s $\tuple[\textsl{nil}]{Δ}{(\Trefl 0)}$ doesn't have type
+  $\id{NList}~\alpha~0$:
+  \begin{itemize}
+  \item We need a weakening constructor to coerce from $\tau_1$ to
+    $\TUnion{\tau_1}{\tau_2}$
+  \end{itemize}
+
+  We also need a strengthening construct, which tests the labels
+\end{myslide}
+
+\renewcommand \righthead {Dessert}
+
+\begin{myslide}{Union types's constructs}
+  \vspace{-15pt}
+  \begin{displaymath}
+    \begin{array}{lc@{;;}c@{;;}l}
+      \textsl{(term)} & e,\tau &::=&
+          ... ~\MAlign{
+        |~ \TUnion{\tau_1}{\tau_2} \
+        |~ \TUcast{\tau_1}{\tau_2}e \
+        |~ {\MAlign{\TUcase {e %% \
+            } {\Ttagvar}{x}{e_\Ttagvar %% \
+            }{y}{e_d}}}
+      }
+    \end{array}
+  \end{displaymath}
+  $\color{mathgreen}\TUcast{\tau_1}{\tau_2}e$ weakens $e$ from ${\tau_1}$ to ${\tau_2}$
+  \begin{itemize}
+  \item Turns into a no-op after type erasure
+  \end{itemize}
+  $\color{mathgreen}\kw{switch}$ jumps to either $e_\Ttagvar$ or $e_d$
+  according to the label on tuple $e$
+  \begin{itemize}
+  \item $e_d$ is a catch-all case; can be chained for multiple branches
+  \item No \emph{boolean blindness}: $x$, $x_\equiv$, $y$, $y_\equiv$ remember the
+    test's result
+  \end{itemize}
+  \SMCenterLine{¡ Builds on labeled tuples and equality types !}
+\end{myslide}
+
+\begin{myslide}{Details of \kw{switch}}
+  \vspace{-10pt}
+  \begin{displaymath}
+    {\MAlign{\TUcase {e %% \
+            } {\Ttagvar}{x}{e_\Ttagvar %% \
+            }{y}{e_d}}}
+  \end{displaymath}
+  $e$ has to have a union type where all alternatives are (labeled) tuples
+
+  $x$ and $y$ are bound to $e$ but with a refined type
+  \begin{itemize}
+  \item $x$ keeps alternatives with label $\Ttagvar$ and $y$ only keeps the
+    others
+  \item For $e : \texttt{NList}~\alpha~n$, if $\Ttagvar$ is $\textsl{nil}$,
+    $x$ has type $\Tuple[\textsl{nil}](\Teq{n}{0})$
+  \item The default branch is not left in the cold:
+    $y : \Tuple[\textsl{cons}](...)$
+  \item The typing rule encodes the usual coverage check
+  \end{itemize}
+
+  $x_\equiv$ (resp $y_\equiv$) is bound to a proof that $x$ (resp $y$) is equal to $e$
+  \begin{itemize}
+  \item Needed for dependent elimination
+  \end{itemize}
+\end{myslide}
+
+\newcommand \Tmu[4][] {\mu_{#1} #2:#3 . #4}
+\newcommand \Tfold[1][\tau~{\vec p}] {\kw{fold}~}%% ~#1
+\newcommand \Tunfold[1][\tau~{\vec p}] {\kw{unfold}~}%% ~#1
+\newcommand \Tletfold[3][\tau~{\vec p}] {\Let{\Tfold[#1]{#2}}{#3}}
+
+\renewcommand \righthead {Coffee}
+
+\begin{myslide}{Recursion}
+  Support for recursive types and recursive functions
+  \begin{displaymath}
+    \begin{array}{lc@{;;}c@{;;}l@{}}
+      %% \textsl{(index)} & i &\in& \mathbb{N} \
+      \textsl{(term)} & e,\tau%% ,p
+      &::=&
+          ... ~\MAlign{
+        |~ \Tmu[i]{x}{\tau}{e}
+        ~|~ \Tmu{x}{\tau}{e} \
+        |~ \Tfold{e}
+        %% ~|~ \Tunfold{e}
+        ~|~ \Tletfold{x}{e_1}{e_2}
+      } \
+    \end{array}
+  \end{displaymath}
+  In principle, these are standard fixpoint constructs
+
+  For the purpose of proving consistency by translation to CIC:
+  \begin{itemize}
+  \item $\color{mathgreen}\Tmu[i]{x}{\tau}{e}$ mimics CIC's recursive functions
+    ($i$ is induction argument)
+  \item $\color{mathgreen}\Tmu{x}{\tau}{e}$ mimics CIC's positivity check
+  \item $\color{mathgreen}\Tletfold{x}{e_1}{e_2}$ is preferred over
+    $\color{mathgreen}\Tunfold{e}$
+  \end{itemize}
+\end{myslide}
+
+\begin{myslide}{Polymorphic variants comparison}
+  Restrictive form of polymorphic variants:
+  \begin{itemize}
+  \item Labels kept abstract: could be small integers
+  \item No polymorphic \kw{case} analysis
+  \item Upcasts need to be explicit
+  \end{itemize}
+  In return we get simple integration into existing PTS
+  \begin{itemize}
+  \item Easily bolted on the side of CC, CCω, ...
+  \end{itemize}
+\end{myslide}
+
+\renewcommand \righthead {The bill}
+
+\begin{myslide}{Conclusion}
+  Defined the Calculus of United Constructions
+  \begin{itemize}
+  \item a lower-level alternative to the Calculus of Inductive Constructions
+  \end{itemize}
+
+  Separates each ingredient of inductive types
+
+  Lends itself to a simple and efficient implementation
+
+  Refines the types even in the default branch of \texttt{switch}
+
+  Proved consistent by translation to the CIC
+\end{myslide}
+
+\begin{myslide}{Future work}
+  Translate all of CIC to CUC
+  \begin{itemize}
+  \item The ingredients are there, but the details still need to be worked out
+  \end{itemize}
+
+  Levitation: Use inductive types to define $\tau_1 \subseteq \tau_2$ and friends
+  \begin{itemize}
+  \item See title of the slide
+  \end{itemize}
+\end{myslide}
+
+\end{document}
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/bece7c8f563acd68ead00ade2bd9d6fda...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/bece7c8f563acd68ead00ade2bd9d6fda...
You're receiving this email because of your account on gitlab.com.





    