We present a kind inference algorithm for the programming language.
The input to the algorithm is source code with (possibly part of)
kind annotations replaced by kind variables. The algorithm infers concrete
kinds for all kind variables.

We ran the algorithm on the test suite by first replacing kind
annotation on all type variables by fresh kind variables, and concluded that
the algorithm correctly infers all kinds. Non surprisingly, we found out that
programmers do not choose the most general kind in 20% of the cases.

§ INTRODUCTION

Software systems usually handle resources such as files
and communication channels.

The correct usage of such resources generally follows a protocol that describes
valid patterns of interactions. For example a file should be opened and
eventually closed, after which no read or write operations should ever be
performed. The case for communication channels is similar: channels are opened,
messages are exchanged, channels may eventually be closed, after which no more
messages should be exchanged.

Session types [6, 7, 15] allow expressing elaborate
protocols (for files and channels, for example) guaranteeing that protocols are
obeyed by programs.

[1, 2, 3] is a concurrent
functional programming language based on System F where processes
communicate via heterogeneously typed-channels governed by context-free
session types [16].

Context-free session types allow describing protocols such as the serialization
of arithmetic expressions. Consider the following datatype for arithmetic

data Exp = Lit Int | Plus Exp Exp | Times Exp Exp

An |Exp| is either a literal with an integer (|Lit Int|), a
sum of two sub-expressions (|Plus Exp Exp|) or the product of two
sub-expressions (|Times Exp Exp|). To serialise a value of type
|Exp| we use a session type such as the following.

type ExpC = +LitC: !Int, PlusC: ExpC;ExpC, TimesC: ExpC;ExpC

The abbreviation |ExpC| defines the type of a channel as seen from the
point of view of the writer. A channel of type |ExpC| offers a set of
options |LitC|, |PlusC| and |TimesC|. If the first
option is chosen, an integer must be sent (|!Int|), while, in the
others, two (sub-) expressions are expected to be sent.

Now, suppose that |serialise| is a function that serialises an
|Exp| on a channel |ExpC|.

serialise : Exp -> ExpC;a -> a

The function expects a channel whose initial part is of type |ExpC|
and then behaves as |a|: |serialise| is thus polymorphic on
|a|. It consumes the front of the channel (of type |ExpC|)
and returns the unused part of the channel (of type |a|).

As simple as it may seem, the above code is not valid in the current version of
. The actual code requires further annotations allowing to distinguish
functional from session types as well as linear from unrestricted types.
The distinction is materialised by classifying types with kinds.

In kinds are composed of a multiplicity and a basic kind. Multiplicities
control the number of times a value may be used: exactly once (linear,
|1|) or zero or more (unrestricted, |*|).
Basic kinds distinguish functional types (|T|) from session types (|S|).

The reason why requires kinds lies on polymorphism. If
|!Int;?Int| is undoubtedly a session type and |Int -> Bool|
a functional type, the same does not apply to the polymorphic variable
|a|. Is it a session type or a functional type? The answer depends on
the base kind of |a|: if |S| or then it is a session type,
if |T| then it is a functional type. Kinds are thus necessary to
decide whether the types such as |a;!Int| are well-formed.

The datatype defined in line 1 is currently written in annotated form as follows.
data Exp:*T = Lit Int | Plus Exp Exp | Times Exp Exp

The kind annotation |*T|, says that the datatype is functional. As for
the multiplicity, we chose the unrestricted usage so that it may be used as
often as required. Notwithstanding, one may declare |Exp| of kind
|1T|, in which case |serialise| must become a linear function
(of type |Exp -> ExpC;a 1-> a|).

Expanding the abbreviation and annotating the datatype in line 2 we get the
following type.
type ExpC:1S = rec a:1S . +LitC: !Int, PlusC: a;a, TimesC: a;a

|ExpC| defines a recursive type that is well-formed when the kind of
its body, the external choice ($\oplus$), is a subkind of the kind for the
recursion variable. In this case, the recursion variable |ExpC| is
annotated with |1S|, given that its body is itself a linear session.

Finally, the function |serialise| is currently written as follows.

serialise : foralla:1S . Exp -> ExpC;a -> a

The polymorphic variable |a| stands for the continuation channel;
it must be a linear session. Annotating |a| with the unrestricted
session |*S| would dictate that it can only be instantiated with
$\TSkip$, the only unrestricted session type.

Even if kinds are necessary in the underlying theory of the language,
they clutter the code.

The code in lines 1–3 is easier to understand and quicker to write; programmers
need not fight the subtleties of each kind. Note that once kinds are inferred,
the prenex occurrences of $\forall$ can be omitted.

The algorithm that we present in this paper annotates all type variables with
their kinds, converting the code in lines 1–3 to that in lines 4–6.

The works more closely related to are Quill [9],
Affe [13], Alms [17],
$\text{F}^{\,\circ}$ [8],
$\text{FuSe}^{\{\}}$ [11] and Linear
Haskell [4]. All these languages feature substructural
type systems for dealing with linear, functional and affine types (in the case
of Affe).

Quill [9] is a language with linear types and a syntax similar to
that of Haskell. Quill features a novel design that combines linear and
functional types. Contrarily to , Quill does not use
kind mechanisms to distinguish between linear and functional types, instead it
uses type predicates (or, qualified types) to reason about linearity.
Furthermore, Quill does not support subkinding. Quill also has a type inference
algorithm which was proven sound and complete.

Affe [13] is an ML-like language with support to linear, affine
and unrestricted types. Like Quill, Affe uses kinds and constrained types to
distinguish between linear and affine types. Affe supports subkinding and it is
equipped with full principal type inference.

Like Affe, Alms [17] is an ML-like language but is based on
$\text{System F}_{<:}^\omega$, the higher-order polymorphic $\lambda$-calculus
with subtyping. Alms supports affine and unrestricted types. It features a rich
kind system with dependent kinds, unions, and intersections. Moreover, Alms supports ML
modules, allows to expose unrestricted types as affine which gives
flexibility to library programmers and it is equipped with local type

$\text{F}^{\,\circ}$ [8] is an extension of System F that
uses kinds to distinguish between linear and unrestricted types. Similarly to
Affe and Alms, it supports subkinding. Similarly to , but unlike Affe,
$\text{F}^{\,\circ}$ does not support quantification over kinds.

The work closest to in terms of context-free session types is
$\text{FuSe}^{\{\}}$ [11]. Padovani proposed an alternative
formulation of context-free session types in which code and types are aligned
via extra annotations, something we decided to avoid in .

Linear Haskell [4] is a proposal to bring linear types to
Haskell. In Linear Haskell functions $T \rightarrow U$ and $T \multimap U$
describe how the arguments of the function are used. The latter form, inspired
by linear logic [5], uses the argument $T$ exactly once. In ,
annotated arrows $\TFun[\un]TU$ or $\TFun[\lin]TU$ describe how the function is
used (unbounded usage or exactly once).

kinding system differentiates session from functional types. It also
classifies types according to their usage, linear or unrestricted. Other systems
consider these notions separately (or only one of them). The ideas behind our
inference algorithm are similar to Quill and Affe, but the details are quite
different since we do not use type qualifiers to reason about linearity.

§ THE SYNTAX OF KINDS, TYPES AND EXPRESSIONS

This section briefly introduces the notions of kinds, types and expressions; we
refer the interested reader to previous work for details [1].
relies on a base set for type variables (denoted by $\typec a$,
$\typec b$, $\typec c$) and another for labels (denoted by $\typec k$,
$\typec \ell$). For the purpose of kind inference, we further use
multiplicity variables (denoted by $\multVar$) and kind variables
(denoted by $\kindVar$).

The syntax of kinds, types and expressions is in <ref>.

(TL) at (0,1.5) $\kindtl$;
(TU) at (-1.5,0) $\kindtu$;
(SL) at (1.5,0) $\kindsl$;
(SU) at (0,-1.5) $\kindsu$;

(TL) – (TU) – (SU) – (SL) – (TL);
(SL) – (TL);
(SU) – (TU);

Multiplicities are used to indicate the number of times a value can be
used. They are either unrestricted ($\un$), which denotes an arbitrary number of
usages, linear ($\lin$), indicating precisely one usage, or a multiplicity
variable ($\multVar$). The kinding system relies on two base kinds: $\prekinds$
for session types and $\prekindt$ for arbitrary types. Kinds are either
the combination of a base kind and a multiplicity or a kind variable $\kindVar$.

Since a value of an unrestricted type may be used zero or more times, and
one with a linear type must be used exactly once, it should be clear that
an unrestricted value can used where a linear one is expected. Similarly, the
interpretation of base kinds should be such that a session type ($\kindsu$,
$\kindsl$) can be used in place of an arbitrary type ($\kindtl$). The subkind
relation for non variables (denoted $\kind \subk \kind$) forms a lattice, as
exhibited in the diagram.

Session types include $\TSkip$ indicating no communication, $\TEnd$
representing channels ready to be closed, output ($\TMsg[\polOut] T$) and input
($\TMsg[\polIn] T$) messages, internal
($\TChoice[\viewIn]{\choice[{\ell}{\colon}{T_\ell}]_{\ell\in L}}$) and external
choices ($\TChoice[\viewOut]{\choice[{\ell}{\colon}{T_\ell}]_{\ell\in L}}$) and
sequential composition ($\TSemi TU$).

Functional types are composed of linear $\TUnit[\lin]$ and unrestricted unit
types $\TUnit[\un]$, linear $\TFun[\lin]TU$ and unrestricted $\TFun[\un]TU$
functions, records $\TRcd\ell TL$, variants $\TVariant\ell TL$ and universal
types $\TAll a\kind T $.

Recursive types $\TRec a \kind T$ are either session or functional depending on
$\kind$. Type variables $\TVar$ may refer to recursion variables in recursive
types or to polymorphic variables in universal types.

A function capturing in its body a free linear variable must itself be

Expressions include variables $\EVar$,

term abstraction $\EAbs{x}{\type}{\expr}$ and application $\EApp ee$,

type abstraction $\ETAbs\TVar\kind\EVal$ and application $\ETApp\expr\type$,

record $\ERcd \ell \expr L$ and record elimination
$\ELet{\ERcd \ell x L}\expr\expr$,

unit $\EUnit$ and unit elimination $\ELet\EUnit\expr\expr$,

injection in a variant $\EApp \ell \expr$ and variant elimination
$\ECase\expr \ell x L$. The expressions for channel operations include channel
creation, $\EApp\ENew\type$, and branching on a choice,
$\EMatch\expr \ell x L$. The remaining operations on channels—namely
$\ENew$, $\ESend$, $\ERcv$ and $\EApp \ESel \ell$—are all understood as
constants (pre-defined variables).

Given that our goal is to infer kind annotations, the reader may wonder why we
allow them in the source language, namely in polymorphic types
$\TAll a\kind T $, in recursive types $\TRec a \kind T$ and in type abstractions
$\ETAbs\TVar\kind\EVal$. Programmers may, if they so wish, provide kind
annotations in the source code. Such annotations are passed to the algorithm.
For those omitted, a fresh kind variable $\kindVar$ is generated in its place.

§ KIND INFERENCE

Our approach to kind inference follows the established two-step process, wherein
the first gathers constraints and the second resolves the constraints.

The constraint generation step produces constraints in two forms:
$\kind\subk\kind$ and
$\multVar = \bigjoin_{\ell\in L}\multFun{\kind[\kindsym_\ell]}$.

The first form represents subkinding constraints, while the second

represents equalities between multiplicity variables and the least upper bound
of a given set of multiplicities. To enhance readability, we use shorthand
notation $\multVar = \multFun{\kind[\kind]}$ for
$\multVar = \bigjoin\multFun{\kind[\kind]}$ and use $\bigjoin$ in infix format
for binary sets.

Constraint Generation from Types

Kind and multiplicity constraints are captured by judgement
The judgement states that type $\type$ has kind $\kind$ under kinding context
$\Delta$ (a map from type variables to kinds), producing constraint set $\cset$.
To clarify the distinction between input and output, we use the subscript
in for parameters and out for results.

We explain a core subset of the constraint generation rules, those in
<ref> (the complete set is in

Rule reads the kind for type variable $\TVar$ (recursive or
polymorphic) from the kinding context, generating no additional restrictions.

Rule governs recursive types which can either be session or
functional. The kind of the recursion variable is copied to the kinding context when
analysing type $\typec T$. A constraint $\kindc{\kind'} \subk \kind$ is
generated to ensure that the kind $\kindc{\kind'}$ of the body of the
recursive type is a subkind of the kind $\kind$ of the recursion variable.

Rule , deals with functions $\TFun{\type}{\type[U]}$. It applies the
algorithm recursively to $\type$ and $\type[U]$, and assigns the kind
$\pKind\mult\prekindt$ to the function type, where $\mult$ comes from the arrow

Rule builds kinds and constraints for all elements in the record. It
generates a new fresh multiplicity variable $\multVar$. The result is kind
$\pKind\multVar\prekindt$ and the constraint set is composed of the union of
$\cset_\ell$ for all $\ell\in L$ and a new constraint associating variable
$\multVar$ to the least upper bound of the multiplicities of
$\kind[\kind_\ell]$. In order to ensure that $\multVar$ gets the expected
multiplicity, all elements must be subkinds of the kind of the record, that is
$\pKind\multVar\prekindt$. Thus, if at least one entry in the record is linear,
then $\multVar$ is also constrained to be linear.

Rule adds the kind of the polymorphic variable to the typing context
when checking the body $\typec T$. It then assigns kind
$\kind[\pKind\multVar\prekindt]$ to the incoming type $\TAll a\kind\type$, where
the fresh multiplicity variable $\multVar$ denotes the multiplicity of the kind
of type $\type$.

Type operator $\syntax{mult}$ is fully resolved only after analysing
expressions. At this point it can only be partially resolved. When applied to a
kind of the form $\pKind\mult\prekind$ operator $\syntax{mult}$ rewrites into
multiplicity $\mult$, that is, $\multFun{\pKind\mult\prekind} = \mult$.

As an example, let us consider the function that extracts the first element of a pair.

\begin{equation*}
\syntax{fst}\colon\TAll a{\kindc{\kindVar_a}}{\TAll b{\kindc{\kindVar_b}}
\end{equation*}

The application of the rules in <ref>, yields the
constraint set
\kind[\multVar_1] = \multFun{\pKind{\multVar_2}\prekindt},
\kind[\multVar_2] = \multFun\kindtu,
\kind[\multVar_3] = \multFun{\kind[\kindVar_a]} \join
\multFun{\kind[\kindVar_b]}
\}$. Solving the
constraint set one obtains
\kind[\multVar_1] = \un,
\kind[\multVar_2] = \un,
\kind[\multVar_3] = \multFun{\kind[\kindVar_a]} \join
\multFun{\kind[\kindVar_b]}
\}$. We resolve the indeterminacy of kind variables $\kind[\kindVar_a]$ and
$\kind[\kindVar_b]$ by assuming that they both are $\kindtl$, the maximum of
the kind lattice.

The solution would then be
$\{\kind[\multVar_1] = \un$, $\kind[\multVar_2] = \un$,
$\kind[\multVar_3] = \lin$,
$\kindc{\kindVar_a} = \kindtl, \kindc{\kindVar_b} = \kindtl\}$.

We argue that assigning $\kindtl$ (the maximum) to $\kindc{\kindVar_a}$ and
$\kindc{\kindVar_b}$ is the preferred solution, since it is the less restrictive
of all solutions. If we were to choose another kind, such as $\kindtu$, then it
would be impossible to call function $ \syntax{fst}$ on linear values (of types
with kind $\kindtl$). We would, undesirably, be ruling out some perfectly
well-behaved programs.

But is $\kindtl$ the best kind for variables $\kindc{\kindVar_a}$ and
$\kindc{\kindVar_b}$? The answer depends on the definition of $\syntax{fst}$.

\begin{equation*}
\syntax{fst} = \ETAbs \TVar {\kindVar_a} {\ETAbs {\TVar[b]} {\kindVar_b}
{{\EAbs[\un] {p} {\TPair{\TVar}{\TVar[b]}} {\ELet{\EPair xy}{p}{x}}}}}
\end{equation*}

An examination of expression $\ELet{\EPair xy}{p}{x}$ reveals that the second
element of the pair, $\termc y$, is discarded. Hence, $\kind[\kindVar_b]$ must
be unrestricted. Would $\kind[\kindVar_b]=\kindtl$ be chosen, then would
complain about a linearity violation when type checking the function. In other
words, constraint $\kind[\kindVar_b] \subk \kindtu$ must be added to the
constraint set, but an inspection of the type of $\syntax{fst}$ alone does not
provide enough information to generate such a constraint. In the following, we
present rules that allow generating constraints such as
$\kind[\kindVar_b] \subk \kindtu$ by inspecting variable usage in expressions.

Constraint Generation from Expressions

Constraints for expressions are derived from judgement
$\cGenE[\Delta_{\text{in}}] {\Gamma_{\text{in}}} {\expr_{\text{in}}}
{\type_{\text{out}}} {\cset_{\text{out}}} {\uset_{\text{out}}}$. The judgement

states that expression $\expr$ has type $\type$ under kinding context $\Delta$
and typing context $\Gamma$. It generates a constraint set $\cset$ and a usage
context $\uset$. Typing contexts map term variables $\termc x$ to types
$\typec T$; usage contexts map term variables $\EVar$ to the kind $\kind$ of
their types. Usage contexts enable reasoning about variable usage: if the
variable is used exactly once, it may be linear, otherwise it must be
unrestricted. Next, we define functions $\weakens$ and $\merges$. The former
checks whether variables are used in expressions. If a variable is not used,
then the set with constraint $\kind\subk\kindtu$ is returned. The latter checks
whether a variable is used more than once: if it appears in multiple usage
contexts, it must also be unrestricted.

We are now in a position to explain the rules for expressions,
in <ref> (the complete set is in <ref>).

Rule is used to assign a type to a variable in a given typing
context. The rule requires the type context $\Gamma$ to contain an entry
$\EVar\colon\type$. The constraints pertaining to type $\type$ are gathered in
$\cset$. To reflect the usage of $\EVar$, the rule returns a singleton map
$\EVar\colon\kind$, where $\kind$ is the kind of $\type$.

Rule deals with abstractions $\EAbs x{\type[T_1]}\expr$. It
recursively calls the judgments on $\type[\type_1]$ and on $\expr$ to collect
constraint sets $\cset_1$, $\cset_2$ and usage context $\uset$. The rule
uses a new predicate, $\isClosures\;\expr$, which holds when $\expr$ is an
abstraction. Then, if $\expr$ is a closure the kind of $\type[\type_1]$ must be
a subkind of $\pKind\mult\prekindt$, where $\mult$ is the multiplicity of the
abstraction. This restriction ensures that unrestricted abstractions do not
close over linear values. The result is type $\TFun{T_1}{T_2}$ together with a
constraint set composed of the union of $\cset_1$, $\cset_2$, $\cset_3$ and the
result of $\weakens$.

The $\weakens$ function checks whether a variable is unused at the end of its
scope. In this case, the lambda abstraction introduces term variable $\EVar$ and
therefore, at the end of the scope, we have to check its usage.

Rule states that if $\expr[\expr_1]$ has type $\TFun{T_1}{T_2}$
and $\expr[\expr_2]$ has type $\type[\type_1]$, then the expression
$\EApp{\expr_1}{\expr_2}$ has type $\type[\type_2]$. The constraints $\cset$ and
usage context $\uset$ are computed by combining the results of the kind
inference of $\expr[\expr_1]$, $\expr[\expr_2]$ and $\type$. The final
constraint set is the union of $\uset_1$, $\uset_2$, $\uset_3$, and the result
of the $\merges$ function which imposes that any variable found in both
$\uset_1$ and $\uset_2$ must be unrestricted. The final usage
context is $\uset_1 \cup \uset_2$.

Rule combines all previously discussed concepts: it evaluates
expressions $\expr[\expr_1]$ and $\expr[\expr_2]$, collecting $\cset_1, \cset_2$
and $\uset_1, \uset_2$. The result is the type of $\expr[\expr_2]$, a constraint
set $\cset$, which is the union of $\cset_1, \cset_2, \cset_3$, the result
of $\merges$ on $\uset_1$ and $\uset_2$,
and the application of $\weakens$ on $\uset_2$ for all
$\expr[x_\ell]\colon\kind[\kindsym_\ell]$ to check for unused variables.

The resulting usage context is the combination of $\uset_1$ and $\uset_2$ with all
entries for $\expr[x_\ell]$ removed.

When analysing constraint generation from the type for function $\syntax{fst}$,
we intuitively concluded that the second element in the pair must be
unrestricted because it is discarded. The application of rules in
<ref>, yield the constraint set
$\{\kindc{\kindVar_b} \subk \kindtu, \kindc{\kindVar_a} \subk
\pKind{\multVar_1}\prekindt, \kindc{\kindVar_b} \subk
\pKind{\multVar_1}\prekindt, \kindc{\kindVar_a} \subk
\pKind{\multVar_0}\prekindt, \kindc{\kindVar_b} \subk
\pKind{\multVar_0}\prekindt, \kindc{\multVar_0} = \multFun{\kindc{\kindVar_a}}
\join \multFun{\kindc{\kindVar_b}}, \kindc{\multVar_1} =
\multFun{\kindc{\kindVar_a}} \join \multFun{\kindc{\kindVar_b}}\}$. A solution
for this set is
$\{\kindc{\multVar_0} = \lin, \kindc{\multVar_1} = \lin, \kindc{\kindVar_a} =
\kindtl, \kindc{\kindVar_b} = \kindtu\}$. The kind variable $\kindc{\kindVar_b}$
is set to $\kindtu$ as we predicted.

The constraint set is computed by combining the constraint sets generated
resulting from applying the judgement to all sub-expressions and the result of
functions $\merges$ and $\weakens$. First, we examine the $\merges$ function: it
takes contexts ${\{{\EVar[p]}\colon{\kind[\kind_p]}\}}$ and
${\{{\EVar[x]}\colon{\kind[\kindVar_a]}\}}$ as input and calculates the
intersection of the two contexts, adding a constraint $\kind\subk\kindtu$ for
each element in the intersection. This process ensures that any variable that is
used in both contexts is unrestricted.

The $\weakens$ function is used to verify if any newly introduced variable is
eventually discarded. In our example, $\weakens$ is applied to
$\EVar\colon{\kind[\kindVar_a]}$ and ${\EVar[y]}\colon{\kind[\kindVar_b]}$
against usage context
$\{{\EVar[p]}\colon{\kind[\kind_p]},\, {\EVar[x]}\colon{\kind[\kindVar_a]}\}$.
For ${\EVar[y]}\colon{\kind[\kindVar_b]}$ function $\weakens$ proceeds as
follows: since $\termc y$ is not present in the context, a new constraint
$\{\kind[\kindVar_b]\subk\kindtu\}$ is added. On the other hand, since $\EVar$
is already in the context, no constraint is created.

Constraint Solving

We now describe an algorithm to solve constraint sets.

* Initialise all kind variables $\kindVar$ to the maximum of the kind
lattice, $\kindtl$. Likewise initialize all multiplicity variables $\multVar$
to the maximum of multiplicities, $\lin$. Store them in $\sigma$.

* Iterate over each constraint in the set:

* If the constraint is of the form $\kind[\kindVar]\subk\kind$, then
update the entry for $\kindVar$ in $\sigma$ with the greatest lower bound of
$\kind$ and $\sigma(\kindVar)$.

For example, if $\sigma = [\kindVar\mapsto\kindtl]$ and we are analysing
constraint $\kindVar\subk\kindtu$, then the value for $\kindVar$ in $\sigma$
must be updated to $\kindtl\meet\kindtu = \kindtu$. After this step, we
would have $\sigma = [\kindVar\mapsto\kindtu]$.

* If the constraint is of the form $\kind\subk\kindVar$, then check whether
$\kind$ and the kind for $\kindVar$ in $\sigma$ is in the subkind relation;
if not then fail. For example, if $\sigma = [\kindVar\mapsto\kindtl]$ and we are
analysing constraint $\kindtu\subk\kindVar$, then we find that it is in the
subkind relation since $\kindtu\subk\kindtl$. A failure would happen with
$\sigma = [\kindVar\mapsto\kindtl]$.

* If the constraint is of the form $\kind[\kind_1]\subk\kind[\kind_2]$ and
neither of the elements is a kind variable, then check whether
$\kind[\kind_1]\subk\kind[\kind_2]$ is in the subkind relation; if not then
fail. If not fail, then remove constraint $\kind[\kind_1]\subk\kind[\kind_2]$
from the constraint set.

* If the constraint is a multiplicity constraint
$\multVar = \bigjoin_{\ell\in L}\multFun{\kind[\kindsym_\ell]}$, then compute the
least upper bound of the multiplicities. If any $\kind[\kindsym_\ell]$ is a
kind variable ($\kindVar$) or a base kind with a multiplicity variable
($\pKind\multVar\prekindt$), we get its kind from $\sigma$ (recall that all
variables are in $\sigma$ as per step 1).

If the thus obtained kind is more restrictive than that for $\multVar$
in $\sigma$ ($\un$ against $\sigma(\multVar) = \lin$), then store it in
$\sigma$. If $\multVar = \un$, then remove the constraint from the set.

* Repeat the process in step 2 until there are no further updates to be made.

* If all constraints have been satisfied, then return the solution $\sigma$.
Otherwise, the constraint set is unsatisfiable.

In the case of function $\syntax{fst}$, the constraints gathered by the rules in
<ref> are as follows.

\begin{gather*}
% \kind[\kindVar_0]\subk\kindtl,
% \kindtu\subk\kindtl,
% \kind[\kindVar_1]\subk\kindtl,
% % \prekindt^{\multVar_0}\subk\kindtu\subk
% \kind[\kindVar_1]\subk\kindtu,
%  % \multVar_4\subk\kindtu\subk
%  %\multVar_3\subk\kindVar_0 \join \kindVar_1\subk
%  % \multVar_2\subk\kindVar_0\join\kindVar_1\subk
%  % \multVar_1\subk\kindVar_0\join\kindVar_1\subk
% \kind[\multVar_0] = \kind[\kindVar_0]\join\kind[\kindVar_1
\kindc{\kindVar_1} \subk {\pKind{\multVar_0}\prekindt},
\kindc{\kindVar_0} \subk {\pKind{\multVar_0}\prekindt},
\kindc{\kindVar_1} \subk {\pKind{\multVar_1}\prekindt},
\kindc{\kindVar_0} \subk {\pKind{\multVar_1}\prekindt},
\kindc{\kindVar_1} \subk \kindtu,
\\
\kindc{\multVar_0} = \multFun{\kindc{\kindVar_0}} \join \multFun{\kindc{\kindVar_1}},
\kindc{\multVar_1} = \multFun{\kindc{\kindVar_0}} \join \multFun{\kindc{\kindVar_1}}
\end{gather*}

We start with
$\sigma = [\kind[\kindVar_0]\mapsto\kindtl, \kind[\kindVar_1]\mapsto\kindtl,
\kindc{\multVar_0}\mapsto\lin, \kind[\multVar_1]\mapsto\lin]$.

Next we pick
constraint $\kindc{\kindVar_1} \subk {\pKind{\multVar_0}\prekindt}$ and use
item 2(a). We have, $\kindc{\kindVar_1} \subk \kindtl$ since
$\sigma(\kindc{\multVar_0}) = \lin$. Given that $\sigma(\kindc{\kindVar_0})$ is
equal to $\kindtl$, and subkinding is reflexive, $\sigma(\kindc{\multVar_0})$
remains as $\kindtl$. The process for the second constraint,
$ \kindc{\kindVar_1}\subk {\pKind{\multVar_0}\prekindt}$, is similar. We
analyse the constraint $\kindc{\kindVar_1}\subk\kindtl$ since
$\sigma(\kindc{\multVar_0}) = \lin$. Also in this case item 2(a) does not
change $\sigma$. The next two constraints,
$\kindc{\kindVar_1} \subk {\pKind{\multVar_1}\prekindt}$ and
$\kindc{\kindVar_0}\subk{\pKind{\multVar_1}\prekindt}$, are also handled by
item 2(a). Once again, $\sigma$ is subject to no update.

Now we pick constraint $\kind[\kindVar_1]\subk\kindtu$. Under item 2(a) the
algorithm computes the greatest lower bound of $\kindtu$ and $\kindtl$, which
is $\kindtu$, so $\sigma$ is updated accordingly.

For the last two constraints we use item 2(d). We read the values of
$\kindc{\kindVar_0}$ and $\kindc{\kindVar_1}$ from $\sigma$ and compute the
least upper bound of $\multFun\kindtl$ and $\multFun\kindtu$ which yields
$\lin$. Both entries for $\kindc{\kindVar_0}$ and $\kindc{\kindVar_1}$ are
already $\lin$ and therefore no update to $\sigma$ is done.

Since we analysed all constraints and $\sigma$ was updated in this iteration of
the algorithm, the fixed-point is not reached yet and so we go through each
constraint once again. This time no update is made and therefore we terminate
$\sigma = [\kind[\kindVar_0]\mapsto\kindtl, \kind[\kindVar_1]\mapsto\kindtu,
\kind[\multVar_0]\mapsto\lin, \kind[\multVar_0]\mapsto\lin]$.

The algorithm iteratively updates the values of the kind and multiplicity
variables until no further updates can be made, that is, until a fixed point is
reached. Since the kind lattice is finite, any sequence of updates must
eventually converge to a fixed point. For the same reason, each constraint can
only be updated a finite number of times. Therefore, the algorithm terminates
after a finite number of iterations.

The running time of the constraint generation algorithm is linear on the size
of the input expression; that of the constraint satisfaction algorithm is
quadratic. In the worst case scenario the number of constraints is equal to the
size of the expression.

Each constraint can only update $\sigma$ twice (when a more restrictive solution
is found). The worst case happens when a different constraint performs an update
in each iteration, forcing the algorithm to analyse all the constraints in each

A sensible optimization removes the constraints from the constraint set also in
items 2(a) and 2(b), after concluding that they cannot update $\sigma$ to a more
restrictive solution. Since the update can only be performed a constant number of
times, the algorithm becomes linear on the size of the input expression.

Category of annotation
1|p5cm|Number of annotations in the source code
1|p5cm|Number of more general annotations generated
Datatypes   129   0

Type abbreviations   206   7

Universal types   282   94

Explicit recursive types   23   10

Type abstractions   30   25
Total   670   136

Distribution of annotations

We implemented the algorithm and incorporated it in the
interpreter. Then we conducted an evaluation to check the
behaviour of the algorithm when used on source code. The evaluation
consisted of replacing all the 670 kind annotations by fresh kind variables in
the 232 valid programs in the test
suite and standard library (total of 9131 lines of code), running the algorithm and checking whether the
algorithm infers the annotations back.

Kind annotations are spread over datatypes, type abbreviations, universal types,
recursive types, and type abstractions. The distribution of annotations is as in

The small number of annotations in recursive types and type abstractions comes
from the fact that they are usually introduced implicitly, either via type
abbreviations (as in the code in line 2) or through compiler
elaboration introducing type abstractions $\ETAbs\TVar\kind\EVal$ for functions
accompanied by their signatures.

We concluded that the algorithm correctly inferred all annotations and found
that 136 of the 670 annotations (that is, 20%) were too specific and could be
relaxed to a more general kind. The largest number of more general annotations
found by the algorithm come from universal types. We attribute this to the
conservative nature of programmers: if we are developing Church encodings (heavy
on polymorphism), why would one require linear type variables? The algorithm did
not improve the kind for datatypes: datatypes are usually used in an
unrestricted manner in programs. Moreover, in the test suite, they usually
appear as the first argument (to be pattern-matched) of functions with
unrestricted closures and therefore they cannot be linear.

For an example where the algorithm suggests a more general kind, consider
function composition.

dot : forall a:*T b:*T c:*T . (b -> c) -> (a -> b) -> a -> c
dot f g x = f (g x)

If we only provide unrestricted arguments to |dot|, then there is no
reason why the polymorphic variables |a|, |b| and
|c| could not have kind |*T|. However, we would be ruling
out programs that apply |dot| to linear arguments. Consider the
following program.

dot : (b -> c) -> (a -> b) -> a -> c
dot f g x = f (g x)

g : ?Int;End -> Int
g c = let (x, c) = receive c in close c ; x

main : Int
main =
let (w,r) = new () in
fork (_ 1-> let w = send 5 w in close w);
dot id g r

This program would be flagged as untypable because we instantiate the
polymorphic variable |a| with the linear session type
|?Int;End|. Since there is no reason why |a|, |b|
and |c| should be unrestricted, the algorithm assigns kind
|1T| to the three polymorphic variables.

§ FUTURE WORK

There are several avenues for future work. The most immediate is to prove the
correctness of the algorithm with respect to the typing system.

Then, equipped with kind inference, we may think of introducing a third base
kind, that for session types that must be eventually closed (that reach type
$\TEnd$). In this case we would require the kind of the argument to function
$\ENew$ to be of the newly introduced kind.

We further plan to study the possibility of quantifying over kinds or
multiplicities for extra flexibility in programming.

We thank the anonymous reviewers for their detailed comments that greatly
contributed to improve the paper. This work was supported by FCT through
project SafeSessions, ref. PTDC/CCI-COM/6453/2020, and the LASIGE Research
Unit, ref. UIDB/00408/2020 and ref. UIDP/00408/2020.

[1]
authorBernardo Almeida,
authorAndreia Mordido,
authorPeter Thiemann &
authorVasco T. Vasconcelos
(year2022): titlePolymorphic lambda calculus
with context-free session types.
journalInf. Comput.
volume289(numberPart), p. pages104948,

[2]
authorBernardo Almeida,
authorAndreia Mordido &
authorVasco T. Vasconcelos
(year2019): titleFreeST, a concurrent
programming language with context-free session types.
noteLast accessed 2023.

[3]
authorBernardo Almeida,
authorAndreia Mordido &
authorVasco T. Vasconcelos
(year2019): titleFreeST: Context-free Session
Types in a Functional Language.
In: booktitlePLACES, seriesEPTCS volume291, pp.
pages12–23, 10.4204/EPTCS.291.2.

[4]
authorJean-Philippe Bernardy,
authorMathieu Boespflug,
authorRyan R. Newton,
authorSimon Peyton Jones &
authorArnaud Spiwack
(year2018): titleLinear Haskell: practical
linearity in a higher-order polymorphic language.
journalProc. ACM Program. Lang.
volume2(numberPOPL), pp.
pages5:1–5:29, 10.1145/3158093.

[5]
authorJean-Yves Girard
(year1987): titleLinear Logic.
journalTheor. Comput. Sci.
volume50, pp. pages1–102,

[6]
authorKohei Honda (year1993):
titleTypes for Dyadic Interaction.
In: booktitleCONCUR, seriesLNCS volume715, publisherSpringer,
pp. pages509–523, 10.1007/3-540-57208-2_35.

[7]
authorKohei Honda,
authorVasco Thudichum Vasconcelos &
authorMakoto Kubo
(year1998): titleLanguage Primitives and Type
Discipline for Structured Communication-Based Programming.
In: booktitleESOP, seriesLNCS volume1381,
publisherSpringer, pp. pages122–138,

[8]
authorKarl Mazurak,
authorJianzhou Zhao &
authorSteve Zdancewic
(year2010): titleLightweight linear types in
system fdegree.
In editorAndrew Kennedy &
editorNick Benton, editors: booktitleProceedings of TLDI 2010: 2010 ACM SIGPLAN
International Workshop on Types in Languages Design and Implementation,
Madrid, Spain, January 23, 2010, publisherACM, pp.
pages77–88, 10.1145/1708016.1708027.

[9]
authorJ. Garrett Morris
(year2016): titleThe best of both worlds: linear
functional programming without compromise.
In editorJacques Garrigue,
editorGabriele Keller &
editorEijiro Sumii, editors: booktitleProceedings of the 21st ACM SIGPLAN International
Conference on Functional Programming, ICFP 2016, Nara, Japan, September
18-22, 2016, publisherACM, pp. pages448–461,

[10]
authorMartin Odersky,
authorChristoph Zenger &
authorMatthias Zenger
(year2001): titleColored local type inference.
In editorChris Hankin &
editorDave Schmidt, editors: booktitleConference Record of POPL 2001: The 28th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London,
UK, January 17-19, 2001, publisherACM, pp.
pages41–53, 10.1145/360204.360207.

[11]
authorLuca Padovani
(year2019): titleContext-Free Session Type
journalACM Trans. Program. Lang. Syst.
volume41(number2), pp. pages9:1–9:37,

[12]
authorBenjamin C. Pierce &
authorDavid N. Turner
(year2000): titleLocal type inference.
journalACM Trans. Program. Lang. Syst.
volume22(number1), pp. pages1–44,

[13]
authorGabriel Radanne,
authorHannes Saffrich &
authorPeter Thiemann
(year2020): titleKindly bent to free us.
journalProc. ACM Program. Lang.
volume4(numberICFP), pp.
pages103:1–103:29, 10.1145/3408985.

[14]
authorJohn C. Reynolds
(year1974): titleTowards a theory of type
In editorBernard J. Robinet,
editor: booktitleProgramming Symposium, Proceedings
Colloque sur la Programmation, Paris, France, April 9-11, 1974, seriesLecture Notes in Computer Science volume19,
publisherSpringer, pp. pages408–423,

[15]
authorKaku Takeuchi,
authorKohei Honda &
authorMakoto Kubo
(year1994): titleAn Interaction-based Language
and its Typing System.
In: booktitlePARLE, seriesLNCS volume817, publisherSpringer,
pp. pages398–413, 10.1007/3-540-58184-7_118.

[16]
authorPeter Thiemann &
authorVasco T. Vasconcelos
(year2016): titleContext-free session types.
In editorJacques Garrigue,
editorGabriele Keller &
editorEijiro Sumii, editors: booktitleProceedings of the 21st ACM SIGPLAN International
Conference on Functional Programming, ICFP 2016, Nara, Japan, September
18-22, 2016, publisherACM, pp. pages462–475,

[17]
authorJesse A. Tov &
authorRiccardo Pucella
(year2011): titlePractical affine types.
In editorThomas Ball &
editorMooly Sagiv, editors: booktitleProceedings of the 38th ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January
26-28, 2011, publisherACM, pp. pages447–458,

[18]
authorJ. B. Wells (year1994):
titleTypability and Type-Checking in the Second-Order
lambda-Calculus are Equivalent and Undecidable.
In: booktitleLICS,
publisherIEEE Computer Society, pp. pages176–185,

[19]
authorAndrew K. Wright
(year1995): titleSimple Imperative
journalLISP Symb. Comput.
volume8(number4), pp. pages343–355.

\begin{gather*}
\axiom{\ruleCGUnit}{\cGenK\TUnit{\kind[\pKind\mult\prekindt]}\Empty}
\quad
\axiom{\ruleCGVar}
% {\TVar a\colon\kind\in\Delta}
{\cGenK[\Delta, \TVar\colon\kind] \TVar\kind\Empty}
\quad
\axiom{\ruleCGSkip}{\cGenK \TSkip\kindsu\Empty}
\quad
\axiom{\ruleCGEnd}{\cGenK \TEnd\kindsl\Empty}
\\
\infrule{\ruleCGMsg}{\cGenK\type\kind\cset}{\cGenK {\TMsg\type} \kindsl\cset}
\quad
\infrule{\ruleCGCh}
{\cGenK{\type[T_\ell]}{\kind[\kindsym_\ell]}{\cset_\ell} \\ (\forall \ell\in L)}
{\cGenK{\TChoice{\recordt\ell TL}}{\kindsl}{\bigcup_{\ell\in L} \cset_\ell \cup \{ \kind[\kind_\ell]\subk\kindsl\}}}
\\
\infrule{\ruleCGSeq}
{\cGenK \type{\kind[\kindsym_1]}{\cset_1} \\
\cGenK {\type[U]}{\kind[\kindsym_2]}{\cset_2}\\
\multVar\;\text{fresh}
{\cGenK {\TSemi\type{\type[U]}}{\pKind\multVar\prekinds}{\cset_1 \cup \cset_2 \cup
\{{\kind[\kindsym_1]} \subk \kindsl,
{\kind[\kindsym_2]} \subk \kindsl,
\multVar = \multFun{\kind[\kindsym_1]} \join \multFun{\kind[\kindsym_2]}
\}}}
\\
\infrule{\ruleCGRec}
{\cGenK [\Delta, \TVar\colon\kind] \type {\kindc{\kind'}} \cset}
{\cGenK {\TRec a\kind\type} {\kindc{\kind'}}{\cset \cup \{{\kindc{\kind'}} \subk \kind\}}}
\quad
\infrule{\ruleCGArrow}
{\cGenK \type{\kind[\kindsym_1]}{\cset_1} \\
\cGenK {\type[U]}{\kind[\kindsym_2]}{\cset_2}}
{\cGenK{\TFun{\type}{\type[U]}}{\pKind\mult\prekindt}{\cset_1 \cup \cset_2}}
\\
\infrule{\ruleCGRcd}
{\cGenK{\type[T_\ell]}{\kind[\kindsym_\ell]}{\cset_\ell} \\
\multVar\;\text{fresh}\\
(\forall \ell\in L)
{\cGenK{\TRcd\ell TL}{\pKind\multVar\prekindt}
{\bigcup_{\ell\in L}  \cset_\ell \cup
\{\multVar = \bigjoin_{\ell\in L}\multFun{\kind[\kindsym_\ell]}
, \kind[\kind_\ell] \subk \pKind\multVar\prekindt
\}}}
\infrule{\ruleCGTAbs}
{\cGenK[\Delta, \TVar\colon\kind] \type{\kindc{\kind'}}\cset \\\multVar\;\text{fresh}}
{\cGenK {\TAll a\kind\type} {\pKind\multVar\prekindt} {\cset \cup \{\multVar = \multFun{\kindc{\kind'}}\}}}
\end{gather*}

Constraint generation from types (complete set of rules)

\begin{gather*}
\infrule{\rulenameIConst}
\quad
\infrule{\rulenameIVar}
\\
\quad
\infrule{\rulenameIAbs}
{\cGenK{\type[T_1]}\kind\cset_1 \\
\cGenE{\Gamma,\EVar\colon\type[T_1]}\expr{\type[T_2]}{\cset_2}\uset
\\
\cset_3 = \isClosure{\expr}{\{\kind\subk{\pKind\mult\prekindt}\}}{\Empty}
{\cGenE\Gamma{\EAbs x{\type[T_1]}\expr} {\TFun{T_1}{T_2}}
{\cset_1 \cup \cset_2 \cup \cset_3 \cup \weaken{\EVar}{\kind}{\uset}}
\\
\infrule{\rulenameIApp}
\\
\cGenE\Gamma{\expr[e_2]}{\type[T_1]}{\cset_2}{\uset_2}
\\
\cGenK{\TFun{T_1}{T_2}}\kind{\cset_3}
{\cGenE\Gamma{\EApp {e_1}{e_2}}{\type[T_2]}
{\uset_1 \cup \uset_2}}
\\
\infrule{\rulenameITAbs}
\\
\cGenK\type{\kind[\kind']}{\cset_2}
% \\
% \kindVar\,\text{fresh}
{\cGenE\Gamma{\ETAbs \TVar\kind\EVal}{\TAll a\kind\type}
\\
\infrule{\rulenameITApp}
{\cGenK\type{\kind[\kindsym_1]}\cset_1 \\
\cGenE\Gamma\expr{\TAll a{\kind[\kindsym_2]}{\type[U]}}{\cset_2}\uset
{\cGenE\Gamma{\ETApp\expr\type}{\subs \type \TVar{\type[U]}}
\\
\infrule{\rulenameIRcdElim}
{\cGenE\Gamma{\expr[e_1]}{\TRcd\ell TL}{\cset_1}{\uset_1}
\\
\cGenE{\Gamma,(\expr[x_\ell]\colon{\type[T_\ell]})_{\ell\in L}}
\\
\cGenK{\type}\kind{\cset_3}
\\
\cGenK{\type[T_\ell]}{\kind[\kindsym_\ell]}{\cset_\ell}
\\
\cset = \cset_1 \cup \cset_2 \cup \cset_3 \cup \mergeFun{\uset_1}{\uset_2} \cup
\weaken{\expr[x_\ell]}{\kind[\kindsym_\ell]}{\uset_2}
\\
(\forall \ell\in L)
{\cGenE\Gamma{\ELet{\ERcd \ell x L}{e_1}{e_2}}\type
\cset{(\uset_1\cup\uset_2)}\setminus\{ \expr[x_\ell]\colon\kind[\kindsym_\ell] \}_{\ell\in L} }
\\
\infrule{\rulenameIRcd}
\\
\cGenK{\type[T_\ell]}{\kindc{\kind_\ell}}\cset'_\ell
\\
(\forall \ell\in L)
{\cGenE\Gamma{\ERcd \ell v L}{\TRcd\ell TL}
{\cset_\ell \cup \cset'_\ell \cup \merges({\uset_\ell})}
{\bigcup_{\ell\in L} \uset_\ell}
\\
\infrule{\rulenameIVariant}
{ \cGenE\Gamma\expr{\type[T_k]}{\cset_1}\uset
\\
\cGenK{\type[T_\ell]}{\kind[\kindsym_\ell]}\cset_\ell
\\
k\in L
\\
(\forall \ell\in L)
{\cGenE\Gamma{\EApp k\expr}{\TVariant\ell TL}{\cset_1\cup\cset_\ell}\uset}
\\
\infrule{\rulenameICase}
{\cGenE\Gamma\expr{\TVariant\ell TL}{\cset_1}{\uset_1}
\\
\cGenE\Gamma{\expr[e_\ell]}{\TFun{T_\ell}{T}}{\cset_\ell}{\uset_\ell}
\\
\cGenK{\type[T_\ell]}{\kind[\kindsym_\ell]}{\cset'_\ell}
\\
(\forall \ell\in L)
{\cGenE\Gamma{\ECase\expr \ell x L}{\type}
\\
\infrule{\rulenameISel}
{ \cGenK{\type[T_\ell]}{\kind[\kindsym_\ell]}\cset_\ell
\\
\cGenE\Gamma{\expr[e_\ell]}{\TFun{T_\ell}T}{\cset'_\ell}{\uset_\ell}
\\
k\in L
\\
(\forall \ell\in L)
{\cGenE\Gamma{\EApp \ESel k}{\TFun{\TChoice[\viewOut]{\recordt\ell TL}}
{\type[T_k]}} {\cset_\ell \cup \cset'_\ell}{\bigcup_{\ell\in L} \uset_\ell}}
\\
\infrule{\rulenameINew}
{ \cGenK[\Empty]\type\kind\cset
{\cGenE\Gamma{\EApp\ENew\type}{\TPair T{\dual T}}\cset\emptyset}
% \ETAbs{\TVar a}{\kind}{\EVal}
% \cset \quad
% \uset \quad
% \tvarset \quad
% \weaken{x}{\kind}{\uset} \quad
% \mergeFun{\uset_1 \cup \uset_2} \quad
% \mergeFun{\uset_1 \cap \uset_2} \quad
% \typeof{\type}
\end{gather*}

Constraint generation from expressions (complete set of rules)


# HIGGS RARE AND EXOTIC DECAYS

LJILJANA MORVAJ 111On behalf of the ATLAS and CMS Collaborations 222Copyright
2021 CERN for the benefit of the ATLAS and CMS Collaborations. Reproduction of
this article or parts of it is allowed as specified in the CC-BY-4.0 license.
CERN, Esplanade des Particules 1,
1217 Meyrin, Switzerland

###### Abstract

Several recent searches for exotic and rare decays of the Standard Model Higgs
boson with the ATLAS and CMS detectors are presented. The searches are
performed on $\sqrt{s}$=13 TeV proton-proton collisions data collected at the
LHC between 2015 and 2018. The topics covered include searches for the Higgs
boson decays into two pseudoscalars, $H\rightarrow aa$, in three different
final states, $2b2\mu$, $4b$ and $2\mu 2\tau$, search for lepton-flavour
violating Higgs decays, $H\rightarrow\mu\tau/e\tau$, and search for a rare
$H\rightarrow\ell\ell\gamma$ decay. ATLAS presents evidence for the
$H\rightarrow\ell\ell\gamma$ rare decay, amounting to an observed significance
of $3.2\sigma$.

##  1 Introduction

Rare and exotic Higgs boson decays searches provide important tests of the
Standard Model (SM) and could lead to a discovery of new physics. Current fits
to the SM Higgs couplings constrain the branching fractions of the Higgs boson
to undetected, $B(H\rightarrow$ undetected), and invisible, $B(H\rightarrow$
invisible), final states to be less than 19% and 9%, respectively [1]. This
leaves a lot of space for new physics in the Higgs boson decays. This talk
presents several recent results delivered by the ATLAS [2] and CMS [3]
collaborations using 13 TeV proton-proton collision data collected at the LHC.
Three types of searches are covered: Higgs decays into beyond-the-SM (BSM)
states ($H\rightarrow aa\rightarrow 2b2\mu/4b/2\mu 2\tau$), lepton flavor
violating Higgs decays ($H\rightarrow\mu\tau/e\tau$) and rare Higgs decays
($H\rightarrow\ell\ell\gamma$).

##  2 Higgs decays to pseudoscalars

Light bosons appear in many well-motivated extensions of the Standard Model.
For example, they could be mediators between the SM and some hidden sector
that does not interact through the weak, strong or electromagnetic forces [4].
Searches for light pseudoscalars in Higgs boson decays are often interpreted
in Two-Higgs-Doublets plus a Singlet (2HDM+S) set of models [4]. The
pseudoscalar component of the singlet field ($a$) acquires Yukawa-like
couplings to SM particles through mixing with Higgs bosons. This implies that
the largest branching fractions of the $a$-boson will generally be to
$b-$quarks and $\tau-$leptons. For $a$-masses ($m_{a}$) that are significantly
lower than the SM Higgs boson mass, the $a$-boson is boosted and its decay
products are collimated. Merging of $b$-jets and hadronically decaying
$\tau$-leptons into one reconstructed object starts below roughly $m_{a}$=25
GeV. ATLAS and CMS have developed dedicated reconstruction and identification
techniques to address such boosted final states.

###  2.1 $H\rightarrow aa\rightarrow 2b2\mu$

The final state with two $b$-jets and two muons [5] provides a good balance
between the typically large decay fraction of $a\rightarrow bb$ and a clean
signature of a narrow dimuon resonance from the $a\rightarrow\mu\mu$ side.
This feature of the decays is further exploited in a kinematic-likelihood (KL)
fit. In the fit, the di-$b$-jet mass ($m_{bb}$) is constrained, within its
resolution, to the dimuon mass ($m_{\mu\mu}$) measured with approximately ten
times better resolution. The output of the KL fit is the maximum likelihood
score, which can be used to select events satisfying the $m_{bb}\sim
m_{\mu\mu}$ hypothesis with high efficiency for the signal, while rejecting a
large portion of SM backgrounds. A Boosted Decision Tree (BDT) discriminant is
trained to discriminate the signal against the dominant backgrounds consisting
of top-quark pair ($t\bar{t}$) and Drell-Yan (DY) production. A number of
kinematic variables characterising event topology are used in the BDT
training. For example, small (large) angular separation between the two
$b$-jets (between the dimuon and the di-$b$-jets systems) characterises the
signal topology at lower $m_{a}$, while the opposite is true for higher
$m_{a}$. The BDT training is done separately at each signal mass in order to
maximally exploit mass-dependent signal characteristics and maximise the
sensitivity across the considered $m_{a}$ range. The dimuon invariant mass
spectrum is scanned in 2 GeV or 3 GeV wide bins in search for an excess above
the background model. The background expectations and the observed data in all
the bins are shown in Figure 1. The largest deviation is observed at 52 GeV
and corresponds to a local (global) significance of 3.3$\sigma$ (1.7$\sigma$).
The upper limits on $B(H\rightarrow aa\rightarrow 2b2\mu)$ are shown in Figure
2, left, in red (observed) and black (expected). The limits are compared to
the result from an earlier ATLAS publication based on 36 fb-1of data [6] (blue
lines) and show factors 2–5 improvement over the full mass range.

Figure 1: Observed data and estimated backgrounds in all $m_{\mu\mu}$ bins
that are tested for the presence of signal in $H\rightarrow aa\rightarrow
2b2\mu$ analysis [5]. The bins are 2 GeV (3 GeV) wide in $m_{\mu\mu}$ for
$m_{a}\leq 45$ GeV ($m_{a}>45$ GeV). Events in neighbouring bins partially
overlap. The bottom panel shows the pull in each bin, defined as
$(n_{\mathrm{obs}}-n_{\mathrm{pred}})/\sigma_{\mathrm{tot}}$, where
$n_{\mathrm{obs}}$ is the number of events in the data, $n_{\mathrm{pred}}$ is
the number of the fitted background events and $\sigma_{\mathrm{tot}}$ is the
total (systematic and statistical, added in quadrature) uncertainty on the
fitted background yield.

Figure 2: Upper limits on $B(H\rightarrow aa\rightarrow 2b2\mu)$ obtained with
139 fb-1of data [5] (left) and $\sigma_{ZH}\times B(H\rightarrow aa\rightarrow
4b)$ obtained with 36.1 fb-1of data [7] (right) as a function of the signal
mass. Black and red dots show masses for which the hypothesis testing was
done. Blue lines show comparisons with previously published ATLAS results
based on 36 fb-1of data: $H\rightarrow aa\rightarrow 2b2\mu$ search [6] (left)
and $H\rightarrow aa\rightarrow 4b$ search in the final state with four
resolved $b$-jets [8] (right).

###  2.2 $H\rightarrow aa\rightarrow 4b$

The ATLAS search for boosted pseudoscalars in the 15 $<m_{a}<$ 30 GeV mass
range [7] developed specialised techniques to tag low-mass $a\rightarrow bb$
objects. The analysis uses lepton triggers to target events where the Higgs
boson is produced in association with a $Z$-boson and $Z$-boson decays
leptonically. The $a\rightarrow bb$ reconstruction procedure starts by
reclustering jets with the standard radius parameter of $R=0.4$ into larger
$R=0.8$ jets. Tracks matched to $R=0.8$ jets are clustered into two or three
sub-jets using the Ex$k_{t}$ [9] algorithm. With this procedure, $b$-quarks
are associated to different sub-jets with nearly 100% efficiency. A BDT
discriminant is trained to distinguish $a\rightarrow bb$ from the background
of jets containing only one $b$-quark. Multivariate $b$-tagging scores of the
sub-jets, the angular separation between the sub-jets and the
$p_{\textrm{\tiny{T}}}$ asymmetry,
($p_{\textrm{\tiny{T}}}$${}^{1}-$$p_{\textrm{\tiny{T}}}$${}^{2})/($$p_{\textrm{\tiny{T}}}$${}^{1}+$$p_{\textrm{\tiny{T}}}$${}^{2})$,
are used in the training. Two working points of the tagger are calibrated in
the data using gluon$\rightarrow bb$ events and used to define a set of
control and signal regions with different signal versus background
contributions and different background compositions. The upper limits on
$B(H\rightarrow aa\rightarrow 4b)$ are shown in Figure 2, right. Below
$m_{a}=25$ GeV, there is a significant gain in sensitivity compared to the
resolved analysis [8] shown in blue. At around $m_{a}=20$ GeV, the boosted
analysis is probing the region below $B(H\rightarrow aa\rightarrow 4b)<100$%,
setting a solid ground for future improvements.

###  2.3 $H\rightarrow aa\rightarrow 2\mu 2\tau$

CMS searched for $H\rightarrow aa$ in the $3.6<m_{a}<21$ GeV mass range in the
final state with two muons ($a\rightarrow\mu\mu$), one hadronically decaying
$\tau$ and one leptonically (muon) decaying $\tau$,
$a\rightarrow\tau_{h}\tau_{\mu}$ [10]. In this mass range, the two
$\tau$-leptons are collimated and a specialised reconstruction technique is
developed in order to reconstruct the $a\rightarrow\tau_{h}\tau_{\mu}$ object.
Standard hadron-plus-strips (HPS) algorithm [11] for reconstruction of
$\tau_{h}$ candidates is modified in two ways. Firstly, muons with
$p_{\textrm{\tiny{T}}}$ $>3$ GeV are removed from jets seeding the HPS
algorithm, resulting in a significant increase in
$a\rightarrow\tau_{h}\tau_{\mu}$ reconstruction efficiency at lower masses
(see Figure 3). Secondly, the muon energy is excluded from the $\tau_{h}$
isolation discriminant, resulting in an efficiency increase over the whole
mass range. Standard Model backgrounds are constrained in a 2D unbinned fit to
the dimuon and four-object ($m_{\mu\mu\tau_{h}\tau_{\mu}}$) invariant masses.
The background model fits the data well and no significant excess above the SM
predictions is observed. The upper limits on $B(H\rightarrow aa\rightarrow
2\mu 2\tau)$ are show in Figure 3.

Figure 3: Left: The efficiency of the standard HPS (dashed lines) and
$\tau_{h}\tau_{\mu}$ HPS reconstruction used in $H\rightarrow aa\rightarrow
2\mu 2\tau$ analysis [10] (solid lines) as a function of $m_{a}$. Right: Upper
limits on $\frac{\sigma_{H}}{\sigma_{SM}}B(H\rightarrow aa\rightarrow 2\mu
2\tau)$ as a function of the signal mass.

###  2.4 $H\rightarrow aa$ summary plots

Model independent limits on $B(H\rightarrow aa\rightarrow xxyy)$, where $x$
and $y$ represent various final-state particles, are translated into limits on
$B(H\rightarrow aa)$ under an assumption of a particular 2HDM+S scenario that
specifies $B(aa\rightarrow xxyy)$. Figure 4 shows interpretations of ATLAS and
CMS $H\rightarrow aa$ searches [12, 13] in the Type-III 2HDM+S scenario [4,
14], with the ratio of vacuum expectation values of the two Higgs doublets
tan$\beta$=2. The plots demonstrate how different final states dominate the
sensitivity at different $m_{a}$. In the full mass range the observed limits
are below the current upper limit on $B(H\rightarrow$ undetected) of 19%, i.e.
direct searches for exotic Higgs decays are probing so far unconstrained phase
space.

Figure 4: Overlay of observed and expected upper limits on
$\frac{\sigma_{H}}{\sigma_{SM}}B(H\rightarrow aa)$ in Type-III 2HDM+S scenario
with tan$\beta$=2 for ATLAS [12] (top) and CMS [13] (bottom).

##  3 Lepton-flavor violating decays

###  3.1 $H\rightarrow\mu\tau/e\tau$

Lepton-flavour violating decays of the Higgs boson are searched for by CMS in
four channels: $\mu\tau_{h},\mu\tau_{e},e\tau_{h}$ and $e\tau_{\mu}$ [15]. The
standard HPS algorithm is used to reconstruct $\tau_{h}$. A BDT discriminant
is trained in each channel separately. Typical input variables to the
training, among others, are lepton transverse momenta, $\Delta\phi$ separation
between the leptons and the missing transverse momentum and the transverse
mass. Each channel is further divided into four event categories, based on the
number of jets in the final state and the di-jet invariant mass, to enhance
different Higgs production mechanisms. A simultaneous fit to the BDT
distributions is performed over all channels and categories to extract upper
limits on $B(H\rightarrow\mu\tau)$ and $B(H\rightarrow e\tau)$. The result is
shown in Figure 5. The upper limits set on $B(H\rightarrow\mu\tau)$ and
$B(H\rightarrow e\tau)$ amount to 0.15% and 0.22%, respectively, and improve
previous ATLAS and CMS results by about a factor two.

Figure 5: Observed and expected upper limits on lepton-flavor violating Higgs
branching fractions, $B(H\rightarrow\mu\tau)$ (left) and $B(H\rightarrow
e\tau)$ (right), shown for each event category separately and for all the
categories combined [15].

##  4 Rare decays

###  4.1 $H\rightarrow\ell\ell\gamma$

ATLAS searched for the Higgs boson decay into two leptons (muons or electros)
and a photon, in the kinematic range where the dilepton mass, $m_{\ell\ell}$,
is below 30 GeV [16]. In this mass range, the analysis is mainly sensitive to
dilepton production through $\gamma^{*}$. Multiple event categories, such as
$ee/\mu\mu$ resolved, $ee$ merged, VBF enhanced, are treated separately to
maximise the analysis sensitivity. A dedicated technique to reconstruct merged
electrons is developed to improve the efficiency in this category. The
$H\rightarrow\ell\ell\gamma$ signal is observed with a significance of
3.2$\sigma$, providing a first evidence of this rare Higgs decay. Figure 6
shows the 3-object invariant mass, $m_{\ell\ell\gamma}$, spectrum, with the
combined signal-plus-background model fit to all analysis categories
simultaneously shown with the red curve. The best-fit value of the signal-
strength parameter, defined as the ratio of the observed signal yield to the
signal yield expected in SM, is measured to be $\mu=1.5\pm 0.5$.

Figure 6: The $m_{\ell\ell\gamma}$ distribution from all the event categories
considered in the $H\rightarrow\ell\ell\gamma$ search [16], added with a
category-dependent weight. The red curve shows the combined signal-plus-
background model. The bottom panel shows the residuals of the data with
respect to the non-resonant background component of the signal-plus-background
fit.

##  5 Summary

This presentation summarised several recent searches for rare and exotic Higgs
boson decays carried out by the ATLAS and CMS collaborations. The presented
analyses are based on the data from 13 TeV proton-proton collisions at the
LHC. The searches for Higgs boson decays into BSM particles and lepton-flavor
violating Higgs decays continue to probe so-far unconstrained parameter space.
In the domain of rare Higgs decays, evidence for the rare
$H\rightarrow\ell\ell\gamma$ decays was found in ATLAS, amounting to an
observed significance of $3.2\sigma$.

## References

## References

  * [1] ATLAS Collaboration, ATLAS-CONF-2020-027, http://cdsweb.cern.ch/record/2725733.
  * [2] ATLAS Collaboration, JINST 3 (2008) S08003.
  * [3] CMS Collaboration, JINST 3 (2008) S08004.
  * [4] D. Curtin et al, Phys. Rev. D 90, 075004 (2014).
  * [5] ATLAS Collaboration, ATLAS-CONF-2021-009, http://cdsweb.cern.ch/record/2759283.
  * [6] ATLAS Collaboration, Phys. Lett. B 790, 1 (2019).
  * [7] ATLAS Collaboration, Phys. Rev. D 102, 112006 (2020).
  * [8] ATLAS Collaboration, JHEP 10 (2018) 031.
  * [9] S. Catani et al, Nucl. Phys. B406 (1993) 187.
  * [10] CMS Collaboration, JHEP 08 (2020) 139.
  * [11] CMS Collaboration, JINST 13 (2018) P10005.
  * [12] ATLAS Collaboration, ATL-PHYS-PUB-2021-008, http://cdsweb.cern.ch/record/2758783.
  * [13] CMS Collaboration, https://twiki.cern.ch/twiki/bin/view/CMSPublic/Summary2HDMSRun2.
  * [14] U. Haisch et al, arXiv:1802.02156 [hep-ph].
  * [15] CMS Collaboration, CMS-PAS-HIG-20-009, https://cds.cern.ch/record/2758334.
  * [16] ATLAS Collaboration, arXiv:2103.10322 [hep-ex].