* in the case of the linear arrow $\itrefinfj{(\vec\beta \synlinto \gamma)
}{ (B \synto C)}$, by induction hypothesis, we get $\itsid{\vec\beta} \in
\Ar(\itgpdoc{B})$ and $\itsid\gamma \in \Ar(\itgpd{C})$ such that
$\itmrefinfj{\itsid{\vec\beta} }{ {\vec\beta} }{ \vec\beta }{ B}$ and
$\itmrefinfj{\itsid\gamma }{\gamma }{\gamma }{C}$. We then put $\itsid{\vec\beta
\synlinto \gamma}$ to be $\itsid{\vec\beta} \synlinto \itsid\gamma$, for which we
are able to derive $\itmrefinfj{\itsid{\vec\beta \synlinto \gamma} }{(\vec\beta
\synlinto \gamma) }{(\vec\beta \synlinto \gamma) }{B \synto C}$ using the
corresponding rule for morphisms;

* in the case of the multilinear formation $\itrefinfj{\vec\alpha }{ A}$ for
$\vec\alpha = \seq{\alpha_1,\ldots,\alpha_n}$, by induction hypothesis, we get
$\itsid{\alpha_i} \in \Ar(\itgpd A)$ such that $\itmrefinfj{\itsid{\alpha_i}
}{\alpha_i }{\alpha_i}{A}$ for $i\in \set{1,\ldots,n}$. We then put
$\itsid{\vec\alpha} =
(\unit{},\seq{\itsid{\alpha_1},\ldots,\itsid{\alpha_n}})$, for which we can
easily derive that $\itmrefinfj{\itsid{\vec\alpha} }{\vec\alpha}{\vec\alpha}{
A}$ using the corresponding rule for morphisms.

Given $\phi_1,\phi_2 \in \Ar(\itgpd A)$ ($\widetilde\phi_1,\widetilde\phi_2 \in \Ar(\itgpdoc {A})$), we say that they are
composable when $\tgt(\phi_1) = \src(\phi_2)$ ($\tgt(\widetilde\phi_1) = \src(\widetilde\phi_2)$). It happens that two
composable intersection type morphisms are very similar in their

Given $\phi_1,\phi_2 \in \Ar(\itgpd A)$ such that they are composable, we have

* if $\phi_1 = \itsstarid$, then $A = o$ and $\phi_2 = \itsstarid$;

* if $\phi_1 = \widetilde\phi_1 \synlinto \psi_1$, then

* $A = B \synto C$ for some unique simple types $B$ and $C$,

* $\widetilde\phi_1 \in \Ar(\itgpdoc B)$ and $\psi_1 \in \Ar(\itgpd C)$,

* $\phi_2 = \widetilde\phi_2 \synlinto \psi_2$ for some unique $\widetilde\phi_2 \in
\Ar(\itgpd B)$ and $\psi_1 \in \Ar(\itgpd C)$,

* and $\widetilde\phi_1,\widetilde\phi_2$ ($\psi_1,\psi_2$) are composable.

Similarly, given $\widetilde\phi_1 = (\sigma_1,\seq{\phi_{1,1},\ldots,\phi_{1,n_1}})$ and
$\widetilde\phi_2 = (\sigma_2,\seq{\phi_{2,1},\ldots,\phi_{2,n_2}})$ in $\Ar(\itgpdoc{A})$
for some $n_i \in \N$, $\sigma_i \in \Sgroup_{n_i}$ and intersection type
morphisms $\phi_{i,1},\ldots,\phi_{i,n_i}$ for $i \in \set{1,2}$, such that
$\widetilde\phi_1$ and $\widetilde\phi_2$ are composable, we have that $n_1 = n_2$ and
$\phi_{1,j}$ is composable with $\phi_{2,\sigma_1(j)}$ for $j\in
\set{1,\ldots,n_1}$.

By mutual induction on the derivations of $\phi_1$ and $\widetilde\phi_1$.

Given a simple type $A$ and two composable linear (multilinear)
intersection type morphisms $\phi_1,\phi_2 \in \Ar(\itgpd{A})$ ($\widetilde\phi_1,\widetilde\phi_2 \in \Ar(\itgpdoc{A})$), we now define their
composition $\phi_2 \itscirc \phi_1$ ($\widetilde\phi_2 \itscirc \widetilde\phi_1$) by
mutual induction. We use <Ref> to give a complete
definition with a minimal case analysis:

* we put $\itsstarid \itscirc \itsstarid = \itsstarid \circ \itsstarid$;

* given composable $\phi_1 = \zeta_1 \synlinto \psi_1$ and $\phi_2 = \zeta_2
\synlinto \psi_2$, we put $\phi_2\itscirc\phi_1 = (\zeta_2 \itscirc \zeta_1)
\synlinto (\psi_2 \itscirc \psi_1)$;

* given composable $\widetilde\phi_1 = (\sigma_1,\seq{\psi_{1,1},\ldots,\psi_{1,n}})$ and
$\widetilde\phi_2 = (\sigma_2,\seq{\psi_{2,1},\ldots,\psi_{2,n}})$, we put

\[
\widetilde\phi_2 \itscirc \widetilde\phi_1 = (\sigma_2 \circ \sigma_1,\seq{\psi_{2,\sigma(1)} \itscirc \psi_{1,1},\ldots,\psi_{2,\sigma(n)} \itscirc \psi_{1,n}})
\zbox.
\]

Given a simple type $A$ and a composable linear (multilinear) intersection
type morphism $\phi \in \itgpd{A}$ ($\widetilde\phi \in \Ar(\itgpdoc{A})$), we
now define its inverse $\finv\phi$ ($\finv{\widetilde\phi}$) by induction on
the derivations:

* we put $\finv {\itsstarid} = \itsstarid$;

* given $\phi = \widetilde\phi \synlinto \psi$, we put $\finv\phi = \finv{\widetilde\phi}
\synlinto \finv\psi$;

* given $\widetilde\phi = (\sigma,\seq{\psi_{1},\ldots,\psi_{n}})$, we put $\finv{\widetilde\phi} =

The above operations assemble into a groupoidal structure:

Given a simple type $A$, we have that

* $\itscirc$ is an associative composition operation on $\itgpd A$ ($\itgpdoc {A}$) with $\itsid{}$ as unit, making $\itgpd {A}$ ($\itgpdoc{A}$) a category;

* for every $\phi \in \Ar(\itgpd A)$ ($\widetilde\phi \in \Ar(\itgpdoc
{A})$), we have $\finv\phi \itscirc \phi = \itsid{\src(\phi)}$ and $\phi
\itscirc \finv\phi = \itsid{\tgt(\phi)}$ ($\finv{\widetilde\phi} \itscirc \widetilde\phi
= \itsid{\src(\widetilde\phi)}$ and $\widetilde\phi \itscirc \finv{\widetilde\phi} =
\itsid{\tgt(\widetilde\phi)}$), so that $\itgpd A$ ($\itgpdoc {A}$) is a

By simple inductions.

The functors $K_A$ and $K^\oc_A$ are built as the direct extensions to
symmetries of the ones built in the proof of <Ref>,
since the definition of multilinear intersection type morphisms closely
follows the definition of the action of $\oc$ on groupoids and their

§.§ Resource context groupoid

We recall that we only consider contexts, resource contexts and resource
morphism contexts that are well-formed, so that we will often omit to precise
that such contexts are well-formed for conciseness.

Given a (well-formed) context $\Gamma = (x_1:A_1,\ldots,x_n:A_n)$, we give some
details about the definition of the groupoid $\itgpd\Gamma$: its objects are the
resource contexts $\Theta = (\itrefinfj[x_1 ]{\kappa_1 }{ A_1}, \ldots,\itrefinfj[ x_n ]{\kappa_n
}{ A_n})$, and its morphisms of type $\Theta \to \Theta'$, for another
resource context $\Theta' = (\itrefinfj[x_1 ]{\kappa'_1 }{ A_1}, \ldots,\itrefinfj[ x_n ]{\kappa'_n
}{ A_n})$, are the resource morphisms contexts $\Xi = (\itmrefinfj[x_1]{\theta_1 }{\kappa_1 }{\kappa'_1 }{A_1},\ldots,\itmrefinfj[x_n]{\theta_n }{\kappa_n }{\kappa'_n }{A_n})$. We then write $\src(\Xi)$ for $\Theta$ and $\tgt(\Xi)$
for $\Theta'$. Two resource morphism contexts $\Xi_1$ and $\Xi_2$ of $\itgpd
\Gamma$ defined by

\[
\Xi_i = (\itmrefinfj[x_1]{\theta_{i,1} }{\kappa_{i,1} }{\kappa'_{i,1} }{A_1},\ldots,\itmrefinfj[x_n]{\theta_{i,n} }{\kappa_{i,n} }{\kappa'_{i,n} }{A_n})
\]

are composable when $\tgt(\Xi) = \src(\Xi')$. In this case, we define
their composite as

\[
\Xi_2 \ctxtcirc \Xi_1 = (\itmrefinfj[x_1]{\theta_{2,1} \itscirc \theta_{1,1} }{\kappa_{1,1} }{\kappa'_{2,1} }{A_1},\ldots,\itmrefinfj[x_n]{\theta_{2,n} \itscirc
\theta_{1,n} }{\kappa_{1,n} }{\kappa'_{2,n} }{A_n})
\zbox.
\]

Moreover, given $\Xi$ as above, there is a resource morphism context $\finv \Xi$
defined by

\[
\finv \Xi = (\itmrefinfj[x_1]{\finv\theta_1 }{\kappa'_1 }{\kappa_1 }{A_1},\ldots,\itmrefinfj[x_n]{\finv\theta_n }{\kappa'_n }{\kappa_n }{A_n})
\]

and which is the inverse of $\Xi$. Given a resource context $\Theta =
(\itrefinfj[x_1]{\kappa_1 }{ A_1},\ldots,\itrefinfj[x_n]{\kappa_n }{ A_n})$, there is an
identity resource morphism context $\ctxtid\Theta$ defined by

\[
\ctxtid\Theta
(\itmrefinfj[x_1]{\itsid{\kappa_1} }{\kappa_1 }{\kappa_1 }{A_1},\ldots,\itmrefinfj[x_n]{\itsid{\kappa_n} }{\kappa_n }{\kappa_n }{A_n})
\zbox.
\]

Following what was done in the previous section, we readily have that

$\itgpd \Gamma$ has a structure of groupoid and, as such, it is isomorphic to
the groupoid $\itgpdoc {A_1} \times \cdots \times \itgpdoc {A_n}$.

§.§ Morphisms between derivations

Here, we give more details about the definition of the $\plact{\rho}{(-)}$
operation on families of multilinear intersection type morphisms and resource
morphism contexts.

Let $m \in \N$, $\rho \in \Sgroup_m$. Given a family of morphisms
$(\itmrefinfj{\widetilde\phi_j}{\vec{\alpha}_j }{\vec{\alpha}'_j }{A})_{1 \le j
\le m}$ where $\widetilde\phi_j = (\sigma_j,\seq{\phi_{j,k}}_{1 \le k \le
l_j})$ with $l_j$ the length of $\vec{\alpha}_j$ (and $\vec{\alpha}'_j$) for
every $j \in \set{1,\ldots,m}$, we write $\plact{\rho}{(\widetilde\phi_j)_{1\le
j \le m}}$ for the  multilinear intersection type morphism $\widetilde\phi$
defined by

\[
\widetilde\phi
\qp=
(\plact{\rho}{(\sigma_j)_{1 \le j \le m}},\seq{\phi_{1,k}}_{1 \le k \le l_1} \seqplus \cdots
\seqplus \seq{\phi_{m,k}}_{1 \le k \le l_m})
\]

where $\seq{\phi_{1,k}}_{1 \le k \le l_1} \seqplus \cdots \seqplus
\seq{\phi_{m,k}}_{1 \le k \le l_m}$ is the mere concatenation of the sequences
of morphisms. Note that we then have the refinement

\[
\itmrefinfj{\widetilde\phi}%
{\vec{\alpha}_1 \seqplus \cdots \seqplus \vec{\alpha}_m}%
{\vec{\alpha}'_{\rho^{-1}(1)} \seqplus \cdots \seqplus \vec{\alpha}'_{\rho^{-1}(m)}}{A}
\zbox.
\]

Now, given a family

\[
(\Xi_j)_{1 \le j \le m} =
\le i \le n})_{1 \le j \le m}
\]

of resource morphism contexts, all refining a common context $\Gamma = x_1 :
A_1,\ldots, x_n : A_n$, we define $\rmcplact{\rho}{(\Xi_j)_{1 \le j \le m}}$ as
the resource morphism context

\[
\rmcplact{\rho}{(\Xi_j)_{1 \le j \le m}}
\qp=
(\itmrefinfj[x_{i}]{\plact{\rho}{(\widetilde\phi_{i,j})_{1 \le j \le
m}}}{\vec\alpha_{i,1} \seqplus \cdots \seqplus\vec\alpha_{i,m}}{\vec\alpha_{i,\finv\rho(1)} \seqplus \cdots \seqplus\vec\alpha_{i,\finv\rho(m)}}{A_{i}})_{1 \le i \le n}
\zbox.
\]

§.§ The intersection type groupoid for a term

We now give some details about the definition of the groupoid $\itgpd M$ for a
well-typed $\Gamma \judge M : A$. Given a derivation $\pi$ of
$\itmfj{\Xi}{\Gamma}{M}{\phi}{\alpha}{\alpha'}{A}$, one can define a derivation
$\src(\pi)$ of $\itfj{\dom(\Xi)}{\Gamma}{M}{\alpha}{A}$ and a derivation
$\tgt(\pi)$ of $\itfj{\cod(\Xi)}{\Gamma}{M}{\alpha'}{A}$ by induction on $\pi$
(and similarly for multilinear judgements). We only give the definition of
$\src(\pi)$ in <Ref> since the one of $\tgt(\pi)$ is similar.

\[
\hss
\begin{gathered}
\src\left(
\scalebox{0.7}{$
\inferrule{\incomment{(x_1:A_1,\ldots,x_n:A_n)\ctxtwf\quad}
\itmfj{\ldots, \itmrefinfj[x_i]{(\unit{\set{1}},\seq{\phi})}{\seq{\alpha}}{\seq{\alpha'}}{A_i}, \ldots }%
{}{x_i }{\phi }{\alpha }{\alpha' }{A_i}}
\right) =
\scalebox{0.7}{$
\inferrule{\incomment{(x_1:A_1,\ldots,x_n:A_n)\ctxtwf\quad}
(\itrefinfj{\alpha}{A_i}) }{
\itfj{\ldots, \itrefinfj[x_i]{\seq{\alpha}}{A_i}, \ldots}{x_1:A_1,\ldots,x_n:A_n}{x_i}{\alpha}{A_i}}
\\
\src\left(
\scalebox{0.7}{$
\inferrule{\inferrule{\pi_1}{\itmfj{\Xi}{}{M}{(\widetilde{\phi} \synlinto \psi)}{(\vec{\alpha} \synlinto \beta)}{(\vec{\alpha}' \synlinto \beta')}{A \synto B}}%
\quad%
\inferrule{\pi_2}{\itmfj{\Xi'}{}{N}{\widetilde{\phi}}{\vec{\alpha}}{\vec{\alpha}'}{A}}}%
{\itmfj{\Xi \rmctxtplus\Xi' }{}{M\,N}{\psi }{\beta }{\beta' }{B}}
\right) =
\scalebox{0.7}{$
\inferrule{\inferrule{\src(\pi_1)}{\itfj{\dom(\Xi)}{}{M}{(\vec{\alpha} \synlinto \beta)}{A \synto B}}%
\quad%
\inferrule{\src(\pi_2)}{\itfj{\dom(\Xi')}{\Gamma}{N}{\vec{\alpha}}{A}}}%
{\itfj{\dom(\Xi \rmctxtplus\Xi' )}{\Gamma}{M\,N}{\beta }{B}}
\\
\src\left(
\scalebox{.70}{$
\inferrule{\inferrule{\pi'}{\itmfj{\Xi,\itmrefinfj[x]{\widetilde{\phi}}{\vec{\alpha}}{\vec{\alpha}'}{A}}{}{M}{\psi}{\beta}{\beta'}{B}}}%
{\itmfj{\Xi}{}{\lambda x.\,M}{(\widetilde{\phi} \synlinto \psi)}{(\vec{\alpha} \synlinto \beta)}{(\vec{\alpha}' \synlinto \beta')}{A \synto B}}
\right) =
\scalebox{.70}{$
\inferrule{\inferrule{\src(\pi')}{\itfj{\dom(\Xi),\itrefinfj[x]{\vec{\alpha}}{A}}{\Gamma,x:A}{M}{\beta}{B}}}%
{\itfj{\dom(\Xi)}{\Gamma}{\lambda x.\,M}{(\vec{\alpha} \synlinto \beta)}{A \synto B}}
\\
\src\left(
\scalebox{.70}{$
\inferrule{n\in \N\quad \sigma \in \Sgroup_n\quad \forall i \in
\set{1,\ldots,n},\;\inferrule*{\pi_i}{\itmfj{\Xi_i}{}{M}{\phi_i}{\alpha_i}{\alpha'_i}{A}}}%
{\itmfj{\plact{\sigma}{(\Xi_i)_{1 \le i\le n}}
\right)
\scalebox{.70}{$
\inferrule{%
\text{$\forall i \in \set{1,\ldots,k}$,}\quad%
\inferrule*{\src(\pi_i)}{\itfj{\dom(\Xi_i)}{\Gamma}{M}{\alpha_i}{A}}%
{\itfj{\dom(\plact{\sigma}{(\Xi_i)_{1 \le i\le n}})}{\Gamma}{M}{\seq{\alpha_1,\ldots,\alpha_k}}{A}}
\end{gathered}
\]

The definition of $\src(\pi)$

The correction of this definition relies on the following easy compatibility
property between resource contexts and the $\dom$ operation:

Let $\Gamma$ be a context. We have:

* given two resource morphism contexts $\itmor{\Xi},\itmor{\Xi'} \refin
\Gamma$, we have $\dom(\Xi \ctxtplus \Xi') = \dom(\Xi)
\ctxtplus \dom(\Xi')$;

* given resource morphism contexts $\itmor{\Xi_1},\ldots,\itmor{\Xi_n}
\refin \Gamma$ and $\Sgroup_n$, we have

\[
\dom(\plact{\sigma}{(\Xi_i)_i}) = \dom(\Xi_1) \ctxtplus \cdots \ctxtplus \dom(\Xi_n)
\]

and similarly for $\cod$.

By direct computation.

We can now start the definition of $\itgpd M$. Its objects are the derivations
$\pi$ of $\itfj{\Theta}{\Gamma}{M}{\alpha}{A}$ and its morphisms between two

\[
\pi_s\co \itfj{\Theta}{\Gamma}{M}{\alpha}{A}
\qqand
\pi_t\co \itfj{\Theta'}{\Gamma}{M}{\alpha'}{A}
\]

are the derivations $\pi$ of $\itmfj{\Xi}{\Gamma}{M}{\phi}{\alpha}{\alpha'}{A}$
such that $\src(\pi) = \pi_s$ and $\tgt(\pi) = \pi_t$. Given two composable
morphisms $\pi_1 \co \itmfj{\Xi_1}{\Gamma}{M}{\phi_1}{\alpha}{\alpha'}{A}$ and
$\pi_2 \co \itmfj{\Xi_2}{\Gamma}{M}{\phi_2}{\alpha'}{\alpha''}{A}$, their
composition $\pi_2 \circ \pi_1$ using the rules of

\[
\hss
\begin{gathered}
\scalebox{0.7}{$
\inferrule{\incomment{(x_1:A_1,\ldots,x_n:A_n)\ctxtwf\quad}
% \text{ for some $i \in \set{1,\ldots,n}$}
\itmfj{\ldots, \itmrefinfj[x_i]{(\unit{\set{1}},\seq{\phi_2})}{\seq{\alpha'}}{\seq{\alpha''}}{A_i}, \ldots }%
{}{x_i }{\phi_2}{\alpha'}{\alpha''}{A_i}}
\circ
\scalebox{0.7}{$
\inferrule{\incomment{(x_1:A_1,\ldots,x_n:A_n)\ctxtwf\quad}
\itmfj{\ldots, \itmrefinfj[x_i]{(\unit{\set{1}},\seq{\phi_1})}{\seq{\alpha}}{\seq{\alpha'}}{A_i}, \ldots }%
{}{x_i }{\phi_1 }{\alpha }{\alpha' }{A_i}}
\\
\scalebox{0.7}{$
\inferrule{\incomment{(x_1:A_1,\ldots,x_n:A_n)\ctxtwf\quad}
(\itmrefinfj{\phi_2 \circ \phi_1}{\alpha}{\alpha''}{A_i})
\itmfj{\ldots, \itmrefinfj[x_i]{(\unit{\set{1}},\seq{\phi_2 \circ \phi_1})}{\seq{\alpha}}{\seq{\alpha''}}{A_i}, \ldots }%
{}{x_i}{\phi_2 \circ \phi_1}{\alpha}{\alpha''}{A_i}}
\\
\scalebox{0.7}{$
\inferrule{\inferrule{\pi_{2,1}}{\itmfj{\Xi_2}{}{M}{(\widetilde{\phi}_2 \synlinto \psi_2)}{(\vec{\alpha}' \synlinto \beta')}{(\vec{\alpha}'' \synlinto \beta'')}{A \synto B}}%
\quad%
\inferrule{\pi_{2,2}}{\itmfj{\Xi'_2}{}{N}{\widetilde{\phi}_2}{\vec{\alpha}'}{\vec{\alpha}''}{A}}}%
{\itmfj{\Xi_2 \rmctxtplus\Xi'_2}{}{M\,N}{\psi_2}{\beta'}{\beta''}{B}}
\circ
\scalebox{0.7}{$
\inferrule{\inferrule{\pi_{1,1}}{\itmfj{\Xi_1}{}{M}{(\widetilde{\phi}_1 \synlinto \psi_1)}{(\vec{\alpha} \synlinto \beta)}{(\vec{\alpha}' \synlinto \beta')}{A \synto B}}%
\quad%
\inferrule{\pi_{1,2}}{\itmfj{\Xi'_1}{}{N}{\widetilde{\phi}_1}{\vec{\alpha}}{\vec{\alpha}'}{A}}}%
{\itmfj{\Xi_1 \rmctxtplus\Xi'_1}{}{M\,N}{\psi_1}{\beta }{\beta' }{B}}
\\
\scalebox{0.7}{$
\inferrule{\inferrule{\pi_{2,1}\circ\pi_{1,1}}{\itmfj{\Xi_2 \circ \Xi_1}{}{M}{(\widetilde{\phi}_2 \synlinto \psi_2)\circ(\widetilde{\phi}_1 \synlinto \psi_1)}{(\vec{\alpha} \synlinto \beta)}{(\vec{\alpha}'' \synlinto \beta'')}{A \synto B}}%
\quad%
\inferrule{\pi_{2,2}\circ\pi_{1,2}}{\itmfj{\Xi'_2\circ\Xi'_1}{}{N}{\widetilde{\phi}_2\circ\widetilde{\phi}_1}{\vec{\alpha}}{\vec{\alpha}''}{A}}}%
{\itmfj{(\Xi_2 \rmctxtplus\Xi'_2)\circ(\Xi_1 \rmctxtplus\Xi'_1)}{}{M\,N}{\psi_2\circ\psi_1}{\beta}{\beta''}{B}}
\\
\scalebox{.70}{$
\inferrule{\sigma_2 \in \Sgroup_n\quad \forall i \in
\set{1,\ldots,n},\;\inferrule*{\pi_{2,i}}{\itmfj{\Xi_{2,i}}{}{M}{\phi_{2,i}}{\alpha'_{\finv\sigma_1(i)}}{\alpha''_{\finv\sigma_1(i)}}{A}}}%
{\itmfj{\plact{\sigma_2}{(\Xi_{2,i})_{1 \le i\le n}}
\circ
\scalebox{.70}{$
\inferrule{n\in \N\quad \sigma_1 \in \Sgroup_n\quad \forall i \in
\set{1,\ldots,n},\;\inferrule*{\pi_{1,i}}{\itmfj{\Xi_{1,i}}{}{M}{\phi_{1,i}}{\alpha_i}{\alpha'_i}{A}}}%
{\itmfj{\plact{\sigma_1}{(\Xi_{1,i})_{1 \le i\le n}}
\\
\scalebox{.70}{$
\inferrule{\forall i \in
\set{1,\ldots,n},\;\inferrule*{\pi_{2,\sigma_1(i)}\circ \pi_{1,i}}{\itmfj{\Xi_{2,\sigma_1(i)}\circ\Xi_{1,i}}{}{M}{\phi_{2,\sigma_1(i)}\circ\phi_{1,i}}{\alpha_i}{\alpha''_i}{A}}}%
{\itmfj{(\plact{\sigma_2}{(\Xi_{2,i})_{1 \le i\le n}}) \circ (\plact{\sigma_1}{(\Xi_{1,i})_{1 \le i\le n}})
}{}{M}{(\sigma_2,\seq{\phi_{2,1},\ldots,\phi_{2,n}}) \circ (\sigma_1,\seq{\phi_{1,1},\ldots,\phi_{1,n}})
\\
\scalebox{.70}{$
\inferrule{\inferrule{\pi'_2}{\itmfj{\Xi_2,\itmrefinfj[x]{\widetilde{\phi}_2}{\vec{\alpha}'}{\vec{\alpha}''}{A}}{}{M}{\psi_2}{\beta'}{\beta''}{B}}}%
{\itmfj{\Xi_2}{}{\lambda x.\,M}{(\widetilde{\phi}_2 \synlinto \psi_2)}{(\vec{\alpha}' \synlinto \beta')}{(\vec{\alpha}'' \synlinto \beta'')}{A \synto B}}
\circ
\scalebox{.70}{$
\inferrule{\inferrule{\pi'_1}{\itmfj{\Xi_1,\itmrefinfj[x]{\widetilde{\phi}_1}{\vec{\alpha}}{\vec{\alpha}'}{A}}{}{M}{\psi_1}{\beta}{\beta'}{B}}}%
{\itmfj{\Xi_1}{}{\lambda x.\,M}{(\widetilde{\phi}_1 \synlinto \psi_1)}{(\vec{\alpha} \synlinto \beta)}{(\vec{\alpha}' \synlinto \beta')}{A \synto B}}
\\
\scalebox{.70}{$
\inferrule{\inferrule{\pi'_2 \circ \pi'_1}{\itmfj{\Xi_2 \circ
\Xi_1,\itmrefinfj[x]{\widetilde{\phi}_2
\circ\widetilde{\phi}_1}{\vec{\alpha}}{\vec{\alpha}''}{A}}{}{M}{\psi_2
\circ \psi_1}{\beta}{\beta''}{B}}}%
{\itmfj{\Xi_2 \circ \Xi_1}{}{\lambda x.\,M}{(\widetilde{\phi}_2
\synlinto \psi_2) \circ (\widetilde{\phi}_1 \synlinto \psi_1)}{(\vec{\alpha} \synlinto \beta)}{(\vec{\alpha}'' \synlinto \beta'')}{A \synto B}}
\end{gathered}
\hss
\]

The definition of composition of intersection type morphism

Note that these are the only required rules, since, when $\pi_1$ and $\pi_2$ are
composable, they have the same shape, because they are derivations for the
same term $M$, and the fact that $\tgt(\pi_1) = \src(\pi_2)$ allows one to infer
other constraints. The rules produce derivations of the adequate type since we

The followings hold:

* given composable $\Xi_1,\Xi_2$ and composable $\Xi'_1,\Xi'_2$ that all
refine a context $\Gamma$, we have

\[
(\Xi_2 \ctxtplus \Xi'_2) \circ (\Xi_1 \ctxtplus \Xi'_1) = (\Xi_2 \circ \Xi_1) \ctxtplus (\Xi'_2 \circ \Xi'_1);
\]

* given $n \in \N$ and $\sigma_1,\sigma_2 \in \Sgroup_n$ and resource
morphism contexts $\Xi_{1,1},\ldots,\Xi_{1,n}$ and
$\Xi_{2,1},\ldots,\Xi_{2,n}$ such that they all refine a context $\Gamma$
and $\Xi_{1,i}$ is composable with $\Xi_{2,\sigma_1(i)}$ for every $i \in
\set{1,\ldots,n}$, we have

\[
(\plact{\sigma_2}{(\Xi_{2,i})_{1 \le i\le n}}) \circ (\plact{\sigma_1}{(\Xi_{1,i})_{1 \le i\le n}})
\plact{(\sigma_2 \circ \sigma_1)}{(\Xi_{2,\sigma(i)} \circ \Xi_{1,i})_{1 \le i\le n}}
\zbox.
\]

By direct computation.

By a similar inductive definition, we can define the identity $\id_\pi$ of a
derivation $\pi$ of a judgement $\itfj{\Theta}{\Gamma}{M}{\alpha}{A}$. Moreover,
following the definition of inverses for intersection type morphisms, we can
define the inverse $\finv\pi$ of a derivation $\pi$ of a judgement
$\itmfj{\Xi}{\Gamma}{M}{\phi}{\alpha}{\alpha'}{A}$. It is then routine to check that

The above operations equip $\itgpd M$ with a structure of groupoid.

§.§ The correspondence interpretation/derivation correspondence

In fact, we prove the following stronger statement:

Let $\Gamma$ be a well-typed context. Given a derivation of $\Gamma
\judge M : A$, there is a canonical morphism of groupoid $K_M \co
\terminterp M \to \itgpd M$ ($K^\oc_M \co \terminterpoc M \to \itgpdoc M$)
making the squares of the following diagram commute:

\begin{equation}
\label{eq:thm:charact-terminterp:cd}
\begin{tikzcd}
\ctxtinterp\Gamma
\ar[d,"K_\Gamma"']
\terminterp M
\ar[l,"{\stdisp[\altidisp{\ctxtinterp\Gamma}{l}]{\terminterp M}}"']
\ar[r,"{\stdisp[\altidisp{\typeinterp A}{r}]{\terminterp M}}"]
\ar[d,"K_M"]
\typeinterp A
\ar[d,"K_A"]
\\
\itgpd\Gamma
\itgpd M
\ar[l,"{\stdisp[l]{M}}"]
\ar[r,"{\stdisp[r]{M}}"']
\itgpd A
\end{tikzcd}
\qquad
\left(
\text{\resp}
\begin{tikzcd}
\ctxtinterp\Gamma
\ar[d,"K_\Gamma"']
\terminterpoc M
% \ar[l,"{\stdisp[\ctxtinterp\Gamma]{\terminterp M}}"']
% \ar[r,"{\stdisp[\typeinterp {\oc A}]{\terminterp M}}"]
\ar[l,"{\stdisp[l]{\terminterpoc M}}"']
\ar[r,"{\stdisp[r]{\terminterpoc M}}"]
\ar[d,"K^\oc_M"]
\oc \typeinterp {A}
\ar[d,"K^\oc_{A}"]
\\
\itgpd\Gamma
\itgpdoc M
% \ar[l,"{\stdisp[\Gamma]{M}}"]
% \ar[r,"{\stdisp[\oc A]{M}}"']
\ar[l,"{\stdispoc[l]{M}}"]
\ar[r,"{\stdispoc[r]{M}}"']
\itgpdoc {A}
\end{tikzcd}
\right)
\zbox.
\end{equation}

We prove it by induction on a derivation of $\Gamma \judge M : A$:

* in the case of the variable typing rule $x_1: A_1,\ldots,x_n: A_n \judge
x_i : A_i$, $K_M$ is defined as the functor sending $u \co a \to a'
\in \typeinterp A = \terminterp {x_i}$ to the unique derivation of

\[
\begin{split}
&\hskip-3em (\itmrefinfj[x_1]{\seq{} }{\seq{} }{\seq{} }{A_1},\ldots,
\itmrefinfj[x_i]{(\unit{\set{1}},\seq{K_{A_i}(u)})}{\seq{K_{A_i}(a)}}{\seq{K_{A_i}(a')}}{A_i},\\
&\ldots,\itmrefinfj[x_n]{\seq{} }{\seq{} }{\seq{}}{A_n}) \refin \Gamma
\judgel x : \itmor{K_{A_i}(u)} \itsco \itype{K_{A_i}(a)} \itsto
\itype{\seq{K_{A_i}(a')}} \refin A_i
\zbox.
\end{split}
\]

It is immediate that the squares of (<ref>)
commute for this definition;

* in the case of an application $\Gamma \judge M\, N: B$, we
have that there exists a unique simple type $A$ such that $\Gamma
\judge N : A$, so that the typing of the application $M\, N$ is constructed
from two derivations $\Gamma \judge M : A \synto B$ and $\Gamma \judge N :
A$. We then have by the rules for intersection type morphism judgements that
$\itgpd {M\,N}$ is the pullback

\[
\begin{tikzcd}
\itgpd {M\,N}
\ar[rr,"P_N",dashed]
\ar[d,"P_M"',dashed]
\phar[rd,very near start,"\drcorner"]
\itgpdoc{N}
\ar[d,"{\stdisp[r]{N}}"]
\\
\itgpd M
\ar[r,"{\stdisp[r]M}"']
\itgpd{A \synto B}
\ar[r,"P^{A\synto B}_A"']
\itgpdoc A
\zbox.
\end{tikzcd}
\]

where $P^{A\synto B}_A$ is the functor projecting a derivation of
$\itmrefinfj{\widetilde{\phi} \synlinto
\psi}{\vec\alpha\linto\beta}{\vec\alpha'\linto\beta}{A \synto B}$ to the
associated derivation
$\itmrefinfj{\widetilde{\phi}}{\vec\alpha}{\vec\alpha'}{A}$. Similarly, by
considering again the definition of the groupoid $\terminterp{M\,N}$, we see
that it can be alternatively expressed as the pullback

\[
\begin{tikzcd}
\terminterp {M\,N}
\ar[rr,"P'_N",dashed]
\ar[d,"P'_M"',dashed]
\phar[rd,very near start,"\drcorner"]
\terminterp{N}^{\oc}
\ar[d,"{\stdisp[r]{\terminterpoc{N}}}"]
\\
\terminterp M
\ar[r,"{\stdisp[r]{\terminterp M}}"']
\oc\typeinterp{A} \times \typeinterp B
\ar[r,"{\pl}"']
\oc \typeinterp A
\zbox.
\end{tikzcd}
\]

Then, using $K^\oc_A$ and the inductively defined $K_M$, $K^\oc_N$, we build
an isomorphism between the underlying cospans of these pullbacks, so that we
get a factorizing isomorphism $K_{M\,N} \co \terminterp {M\,N} \to
\itgpd{M\,N}$. Concerning the commutativity condition we have the diagram

\[
\begin{tikzcd}
\ctxtinterp \Gamma
\ar[d,"K_{\Gamma}"']
\ctxtinterp \Gamma \times \ctxtinterp \Gamma
\ar[l,"(\ctxtplus)"']
\ar[d,"K_{\Gamma}\times K_{\Gamma}"{description}]
\terminterp M \times \terminterpoc N
\ar[l,"{\stdisp[l]{\terminterp M} \times \stdisp[l]{\terminterpoc N}}"']
\ar[d,"K_{M}\times K_N"{description}]
\terminterp {M\,N}
\ar[l,"{(P'_M,P'_N)}"']
\ar[d,"K_{M\,N}"]
\\
\itgpd \Gamma
\itgpd \Gamma \times \itgpd \Gamma
\ar[l,"(\ctxtplus)"]
\itgpd M \times \itgpdoc N
\ar[l,"{\stdisp[l]{M}\times\stdispoc[l]{N}}"]
\itgpd {M\,N}
\ar[l,"{(P_M,P_N)}"]
\end{tikzcd}
\]

where each rectangle commutes and the top row is precisely
$\stdisp[l]{\terminterp{M\,N}}$ and the bottom row $\stdisp[l]{M\,N}$.

On the side of $B$, we have the diagram

\[
\begin{tikzcd}
\terminterp{M\,N}
\ar[r,"P'_M"]
\ar[d,"K_{M\,N}"']
\terminterp M
\ar[r,"{\stdisp[r]{\terminterp{M}}}"]
\ar[d,"K_{M}"{description}]
\oc \typeinterp {A} \times \typeinterp{B}
\ar[r,"\pr"]
\ar[d,"K_{A\synto B}"{description}]
\typeinterp {B}
\ar[d,"K_{B}"]
\\
\itgpd{M\,N}
\ar[r,"P_M"']
\itgpd{M}
\ar[r,"{\stdisp[r]{M}}"']
\itgpd {A \synto B}
\ar[r,"P^{A\synto B}_B"']
\itgpd B
\end{tikzcd}
\]

where $P^{A\synto B}_B$ is defined like $P^{A\synto B}_A$, where every
rectangle commutes, where the top row is $\stdisp[r]{\terminterp{M\,N}}$ and
the bottom row is $\stdisp[r]{M\,N}$. Which concludes the proof of the
commutativity conditions;

* in the case of a $\lambda$-abstraction $\Gamma\judge \lambda x.M: A
\synto B$, we get by induction the commutative diagram

\[
\begin{tikzcd}
\ctxtinterp{\Gamma,x:A}
\ar[d,"K_{(\Gamma,x:A)}"']
\terminterp M
\ar[l,"{\stdisp[l]{\terminterp M}}"']
\ar[r,"{\stdisp[r]{\terminterp M}}"]
\ar[d,"K_{M}"{description}]
\typeinterp B
\ar[d,"K_{B}"]
\\
\itgpd{\Gamma,x:A}
\itgpd M
\ar[l,"{\stdisp[l]{M}}"]
\ar[r,"{\stdisp[r]{M}}"']
\itgpd B
\end{tikzcd}
\]

so that, using the isomorphisms $\ctxtinterp{\Gamma,x:A} \cong
\ctxtinterp\Gamma \times \oc \typeinterp A$, $\itgpd{\Gamma,x:A} \cong \itgpd
\Gamma \times \itgpdoc A$, $\oc \typeinterp A \times \typeinterp B \cong
\typeinterp{A \synto B}$ and $\itgpdoc A \times \itgpd B \cong \itgpd {A
\synto B}$, we are able to get a similar commutative diagram for $\lambda
x. M$;

* finally, we define the multilinear interpretation of a judgement $\Gamma
\judge M : A$ from the above cases: we have a commutative diagram

\[
\begin{tikzcd}
\ctxtinterp \Gamma
\ar[d,equals]
\terminterpoc M
% \ar[ll,"{\stdisp[\ctxtinterp\Gamma]{\terminterpoc M}}"']
% \ar[r,"{\stdisp[\oc \typeinterp A]{\terminterpoc M}}"]
\ar[ll,"{\stdisp[l]{\terminterpoc M}}"']
\ar[r,"{\stdisp[r]{\terminterpoc M}}"]
\ar[d,equals]
\oc \typeinterp A
\ar[d,equals]
\\
\ctxtinterp \Gamma
\ar[d,"K_\Gamma"{description}]
\oc \ctxtinterp \Gamma
\ar[l,"\ctxtmu_\Gamma"']
\ar[d,"\oc K_\Gamma"{description}]
\oc \terminterp {M}
% \ar[l,"{\oc\stdisp[\ctxtinterp\Gamma]{\terminterp{M}}}"']
% \ar[r,"{\oc\stdisp[\typeinterp A]{\terminterp{M}}}"]
\ar[l,"{\oc\stdisp[l]{\terminterp{M}}}"']
\ar[r,"{\oc\stdisp[r]{\terminterp{M}}}"]
\ar[d,"\oc K_{M}"{description}]
\oc \typeinterp A
\ar[d,"\oc K_A"{description}]
\\
\itgpd \Gamma
\ar[d,equals]
\oc \itgpd \Gamma
\ar[l,"{\itsctxtmu_\Gamma}"']
\oc \itgpd {M}
\ar[l,"{\oc\stdisp[l]{M}}"']
\ar[r,"{\oc\stdisp[r]{M}}"]
\ar[d,"\sim"{description}]
\oc \itgpd A
\ar[d,"\sim"{description}]
\\
\itgpd \Gamma
\itgpdoc {M}
\ar[ll,"{\stdispoc[l]{M}}"']
\ar[r,"{\stdispoc[r]{M}}"]
\itgpdoc {A}
\end{tikzcd}
\]

where the morphism $\oc \itgpd {M} \xto\sim \itgpdoc {M}$ is basically the
multilinear introduction rule—a sequence $\seq{\pi_i}_{1\le i \le n}$ of
derivations $\pi_i$ of $\itfj{\Theta_i}{\Gamma}{M}{\alpha_i}{A}$ is mapped
to the derivation of $\itfj{\Theta_1 \ctxtplus \cdots \ctxtplus
\Theta_n}{\Gamma}{M}{\seq{\alpha_1,\ldots,\alpha_n}}{A}$ and similarly for
sequences of morphism derivations—and the morphism $\oc \itgpd A \xto\sim
\itgpdoc{A}$ is similarly the multilinear refinement introduction rule, and
$\itsctxtmu$ is the functor mapping a sequence of resource contexts
$\seq{\Theta_1,\ldots,\Theta_n} \in \Ob(\oc\itgpd\Gamma)$ to $\Theta_1
\rctxtplus \ldots \rctxtplus \Theta_n$ and a morphism
$(\sigma,\seq{\Xi_i}_{1 \le i \le n}) \in \Ar(\itgpd\Gamma)$ between two
sequences $\seq{\Theta_1,\ldots,\Theta_n}$ and
$\seq{\Theta'_1,\ldots,\Theta'_n}$ to $\rmcplact{\sigma}{(\Xi_i)_{1 \le i
\le n}}$. It is quite immediate to check that every rectangle commutes.

§ POSTPONED PROOFS FOR RELATIONAL COLLAPSES

§.§ Functoriality of the collapse to $\Rel$

We give the postponed proof of the following result:

It is obvious that the identity span $A \ot A \to A$ is sent to the
identity relation on $\syms{A}$. For functoriality, it is obvious by
definition that $\syms{T\odot S} \subseteq \syms{T} \circ \syms{S}$ –
but the other direction is not, since composition in $\Thin$ is more
constrained than in $\Rel$.

So consider $(\ca, \cb) \in \syms{S}$ and $(\cb, \cc) \in \syms{T}$.
definition, there are $s \in S$ such that $\ca = \class{s_A}$ and $\cb
= \class{s_B}$, and $t \in T$ such that $\cb = \class{t_B}$ and $\cc =
\class{t_C}$. Since $\class{s_B} = \class{t_B}$ those two are
symmetric, but they might not be equal, meaning that the pair $(s, t)$
may not be a valid element of $T \odot S$. However, by Lemma
there must be $\varphi^S \in S[s, s']$ and $\varphi^T \in T[t, t']$
such that $s'_B = t'_B$ and we can now form $(s', t') \in T\odot S$
with $\class{(s', t')_A} = s'_A = \ca$ and $\class{(s', t')_C} =
\class{t'_C} = \cc$ as required.

§.§ Bijection for the quantitative collapse

From $(\theta_A^-, s, \theta_B^+)$ and $(\Omega_B^-, t, \Omega_B^+)$,
we can apply Lemma <ref> and compose $s$ and $t$ via
$\Omega_B^- \circ \theta_B^+$, giving us unique $\omega^S, \nu^T$
such that the big rectangle commutes, $\omega^S_A$ negative and
$\nu^T_C$ positive. We get $\Theta$ as either path around the
rectangle, and $\psi^-_A, \psi^+_C$ by composition. Reciprocally, from
$(\psi_A^-, s', \Theta, t', \psi_C^+)$ we obtain uniquely the remaining
data by Proposition <ref>.

§ SEELY FUNCTORS AND THEIR KLEISLI LIFTING

Here we include a few folkore results that we required regarding the
adequate definition of morphisms between Seely categories, along with
the fact that they admit a lifting to cartesian closed functors between
the Kleisli categories.

Consider $\catC$ and $\catD$ two Seely categories.

A Seely functor $F : \catC \to \catD$ is a functor,
additionally equipped with isomorphisms

\[
\begin{array}{rcrcl}
t^\oc_A &:& \oc F A &\to& F \oc A\\
t^\tensor_{A, B} &:& F A \tensor FB &\to& F(A\tensor B)\\
t^\with_{A, B} &:& FA \with FB &\to & F(A \with B)\\
t^\lin_{A, B} &:& FA \lin FB &\to& F(A \lin B)
\end{array}
\]

such that $t^\oc_A$ is natural in $A$ and $t^\tensor_{A, B}$ is natural
in $A$ and $B$, and subject to the following coherence conditions:

\[
\xymatrix{
&\oc FA	\ar[rr]^{t^\oc_A}
\ar[dl]_{\delta^\catD_{FA}}&&
F\oc A	\ar[dr]^{F \delta^\catC_A}\\
\oc \oc FA
\ar[rr]_{\oc t^\oc_A}&&
\oc F \oc A
\ar[rr]_{t^{\oc}_{\oc A}}&&
F\oc \oc A
\xymatrix{
\oc FA	\ar[rr]^{t^\oc_A}
\ar[dr]_{\epsilon^\catD_{FA}}&&
F\oc A	\ar[dl]^{F \epsilon^\catC_A}\\
\]

\[
\xymatrix@R=20pt@C=20pt{
&\oc FA \tensor \oc F B
\ar[dl]_{\see^\catD_{FA, FB}}
\ar[dr]^{t^\oc_A \tensor t^\oc_B}\\
\oc (FA \with FB)
\ar[d]_{\oc t^\with_{A, B}}&&
F\oc A \tensor F\oc B
\ar[d]^{t^\tensor_{\oc A, \oc B}}\\
\oc F(A\with B)
\ar[dr]_{t^\oc_{A \with B}}&&
F(\oc A \tensor \oc B)
\ar[dl]^{F \see^\catC_{A, B}}\\
&F\oc (A \with B)
\xymatrix{
&FA \with FB
\ar[dl]_{\pi^\catD_1}
\ar[dd]|{t^\with_{A, B}}
\ar[dr]^{\pi^\catD_2}\\
FA && FB\\
&F(A \with B)
\ar[ul]^{F \pi^\catC_1}
\ar[ur]_{F \pi^\catC_2}
\]

\[
\xymatrix{
(FA \lin FB) \tensor FA
\ar[r]^{t^{\lin}_{A, B} \tensor FA}
\ar[dr]_{\evm^\catD_{FA, FB}}&
F(A\lin B) \tensor FA
\ar[r]^{t^\tensor_{A\lin B, A}}&
F((A \lin B) \tensor A)
\ar[dl]^{F\evm^\catC_{A, B}}\\
\]

The main interest of those is that they lift to cartesian closed
functors between the Kleisli categories:

Consider $\catC$ and $\catD$ two Seely categories, and $F : \catC \to
\catD$ a Seely functor.

Then, defining $F_\oc(A) = F(A)$ on objects and $F_\oc(f) = Ff \circ
t^\oc_A$ for $f \in \catC[\oc A, B]$, we get

\[
F_\oc : \catC_\oc \to \catD_\oc
\]

a cartesian closed functor.

We must show that products and arrows are preserved up to (canonical)
isomorphism. For that, we construct the following morphisms in $\catD$:

\[
\begin{array}{rclcrcl}
k^\with_{A, B} &=& t^\with_{A, B} \circ \epsilon^\catD_{FA \with FB}
&:& \oc (FA \with FB) &\to& F(A\with B)\\
k^\tto_{A, B} &=& t^\lin_{\oc A, B} \circ ((t^\oc_A)^{-1} \lin B) \circ
\epsilon^\catD_{\oc FA \lin FB}
&:& \oc (\oc FA \lin FB)&\to& F(\oc A \lin B)\,,
\end{array}
\]

which we regard as $k^\with_{A, B} \in \catD_{\oc}[FA \with FB,
F(A\with B)]$ and $k^\tto_{A, B} \in \catD_{\oc}[FA \tto FB, F(A\tto
B)]$ where $A \tto B = \oc A \lin B$. By construction those are
isomorphisms, and to show canonicity we must prove (in $\catD_\oc$) the
diagrams corresponding to the last two diagrams of Definition
<ref>, which is a lengthy diagram chase.

§ INTRODUCTION

ACM's consolidated article template, introduced in 2017, provides a
consistent  style for use across ACM publications, and
incorporates accessibility and metadata-extraction functionality
necessary for future Digital Library endeavors. Numerous ACM and
SIG-specific  templates have been examined, and their unique
features incorporated into this single new template.

If you are new to publishing with ACM, this document is a valuable
guide to the process of preparing your work for publication. If you
have published with ACM before, this document provides insight and
instruction into more recent changes to the article template.

The “” document class can be used to prepare articles
for any ACM publication — conference or journal, and for any stage
of publication, from review to final “camera-ready” copy, to the
author's own version, with very few changes to the source.

§ TEMPLATE OVERVIEW

As noted in the introduction, the “” document class can
be used to prepare many different kinds of documentation — a
double-anonymous initial submission of a full-length technical paper, a
two-page SIGGRAPH Emerging Technologies abstract, a “camera-ready”
journal article, a SIGCHI Extended Abstract, and more — all by
selecting the appropriate template style and template parameters.

This document will explain the major features of the document
class. For further information, the  User's Guide is
available from

§.§ Template Styles

The primary parameter given to the “” document class is
the template style which corresponds to the kind of publication
or SIG publishing the work. This parameter is enclosed in square
brackets and is a part of the  command:

Journals use one of three template styles. All but three ACM journals
use the  template style:

* : The default journal template style.

* : Used by JOCCH and TAP.

* : Used by TOG.

The majority of conference proceedings documentation will use the  template style.

* : The default proceedings template style.

* : Used for SIGCHI conference articles.

* : Used for SIGPLAN conference articles.

§.§ Template Parameters

In addition to specifying the template style to be used in
formatting your work, there are a number of template parameters
which modify some part of the applied template style. A complete list
of these parameters can be found in the  User's Guide.

Frequently-used parameters, or combinations of parameters, include:

* : Suitable for a “double-anonymous”
conference submission. Anonymizes the work and includes line
numbers. Use with the  command to print the
submission's unique ID on each page of the work.

* : Produces a version of the work suitable
for posting by the author.

* : Produces colored hyperlinks.

This document uses the following string as the first command in the
source file:

§ MODIFICATIONS

Modifying the template — including but not limited to: adjusting
margins, typeface sizes, line spacing, paragraph and list definitions,
and the use of the  command to manually adjust the
vertical spacing between elements of your work — is not allowed.

Your document will be returned to you for revision if
modifications are discovered.

§ TYPEFACES

The “” document class requires the use of the
“Libertine” typeface family. Your  installation should include
this set of packages. Please do not substitute other typefaces. The
“” and “” packages should not be used,
as they will override the built-in typeface families.

§ TITLE INFORMATION

The title of your work should use capital letters appropriately -
<https://capitalizemytitle.com/> has useful rules for
capitalization. Use the  command to define the title of
your work. If your work has a subtitle, define it with the
command.  Do not insert line breaks in your title.

If your title is lengthy, you must define a short version to be used
in the page headers, to prevent overlapping text. The
command has a “short title” parameter:

§ AUTHORS AND AFFILIATIONS

Each author must be defined separately for accurate metadata
identification.  As an exception, multiple authors may share one
affiliation. Authors' names should not be abbreviated; use full first
names wherever possible. Include authors' e-mail addresses whenever

Grouping authors' names or e-mail addresses, or providing an “e-mail
alias,” as shown below, is not acceptable:

The  and  commands allow a note
to apply to multiple authors — for example, if the first two authors
of an article contributed equally to the work.

If your author list is lengthy, you must define a shortened version of
the list of authors to be used in the page headers, to prevent
overlapping text. The following command should be placed just after
the last  definition:

Omitting this command will force the use of a concatenated list of all
of the authors' names, which may result in overlapping text in the
page headers.

The article template's documentation, available at
<https://www.acm.org/publications/proceedings-template>, has a
complete explanation of these commands and tips for their effective

Note that authors' addresses are mandatory for journal articles.

§ RIGHTS INFORMATION

Authors of any work published by ACM will need to complete a rights
form. Depending on the kind of work, and the rights management choice
made by the author, this may be copyright transfer, permission,
license, or an OA (open access) agreement.

Regardless of the rights management choice, the author will receive a
copy of the completed rights form once it has been submitted. This
form contains  commands that must be copied into the source
document. When the document source is compiled, these commands and
their parameters add formatted text to several areas of the final

* the “ACM Reference Format” text on the first page.

* the “rights management” text on the first page.

* the conference information in the page header(s).

Rights information is unique to the work; if you are preparing several
works for an event, make sure to use the correct set of commands with
each of the works.

The ACM Reference Format text is required for all articles over one
page in length, and is optional for one-page articles (abstracts).

§ CCS CONCEPTS AND USER-DEFINED KEYWORDS

Two elements of the “acmart” document class provide powerful
taxonomic tools for you to help readers find your work in an online

The ACM Computing Classification System —
<https://www.acm.org/publications/class-2012> — is a set of
classifiers and concepts that describe the computing
discipline. Authors can select entries from this classification
system, via <https://dl.acm.org/ccs/ccs.cfm>, and generate the
commands to be included in the  source.

User-defined keywords are a comma-separated list of words and phrases
of the authors' choosing, providing a more flexible way of describing
the research being presented.

CCS concepts and user-defined keywords are required for for all
articles over two pages in length, and are optional for one- and
two-page articles (or abstracts).

§ SECTIONING COMMANDS

Your work should use standard  sectioning commands:
, , , and
. They should be numbered; do not remove the numbering
from the commands.

Simulating a sectioning command by setting the first word or words of
a paragraph in boldface or italicized text is not allowed.

§ TABLES

The “” document class includes the “”
package — <https://ctan.org/pkg/booktabs> — for preparing
high-quality tables.

Table captions are placed above the table.

Because tables cannot be split across pages, the best placement for
them is typically the top of the page nearest their initial cite.  To
ensure this proper “floating” placement of tables, use the
environment table to enclose the table's contents and the
table caption.  The contents of the table itself must go in the
tabular environment, to be aligned properly in rows and
columns, with the desired horizontal and vertical rules.  Again,
detailed instructions on tabular material are found in the
User's Guide.

Immediately following this sentence is the point at which
Table <ref> is included in the input file; compare the
placement of the table here with the table in the printed output of
this document.

Frequency of Special Characters

Non-English or Math   Frequency   Comments

Ø    1 in 1,000    For Swedish names

$\pi$     1 in 5    Common in math

$     4 in 5     Used in business

$\Psi^2_1$     1 in 40,000    Unexplained usage

To set a wider table, which takes up the whole width of the page's
live area, use the environment table* to enclose the table's
contents and the table caption.  As with a single-column table, this
wide table will “float” to a location deemed more
desirable. Immediately following this sentence is the point at which
Table <ref> is included in the input file; again, it is
instructive to compare the placement of the table here with the table
in the printed output of this document.

Some Typical Commands

Command    A Number     Comments

100    Author

300     For tables

400    For wider tables

Always use midrule to separate table header rows from data rows, and
use it only for this purpose. This enables assistive technologies to
recognise table headers and support their users in navigating tables
more easily.

§ MATH EQUATIONS

You may want to display math equations in three distinct styles:
inline, numbered or non-numbered display.  Each of the three are
discussed in the next sections.

§.§ Inline (In-text) Equations

A formula that appears in the running text is called an inline or
in-text formula.  It is produced by the math environment,
which can be invoked with the usual
construction or with
the short form . You can use any of the symbols
and structures, from $\alpha$ to $\omega$, available in
<cit.>; this section will simply show a few
examples of in-text equations in context. Notice how this equation:

set here in in-line math style, looks slightly different when
set in display style.  (See next section).

§.§ Display Equations

A numbered display equation—one set off by vertical space from the
text and centered horizontally—is produced by the equation
environment. An unnumbered display equation is produced by the
displaymath environment.

Again, in either environment, you can use any of the symbols and
structures available in ; this section will just give a couple
of examples of display equations in context.  First, consider the
equation, shown as an inline equation above:

\begin{equation}
\lim_{n\rightarrow \infty}x=0
\end{equation}

Notice how it is formatted somewhat differently in
the displaymath
environment.  Now, we'll enter an unnumbered equation:

∑_i=0^∞ x + 1

and follow it with another numbered equation:

\begin{equation}
\sum_{i=0}^{\infty}x_i=\int_{0}^{\pi+2} f
\end{equation}

just to demonstrate 's able handling of numbering.

§ FIGURES

The “” environment should be used for figures. One or
more images can be placed within a figure. If your figure contains
third-party material, you must clearly identify it as such, as shown
in the example below.

Your figures should contain a caption which describes the figure to
the reader.

Figure captions are placed below the figure.

Every figure should also have a figure description unless it is purely
decorative. These descriptions convey what’s in the image to someone
who cannot see it. They are also used by search engine crawlers for
indexing images, and when images cannot be loaded.

A figure description must be unformatted plain text less than 2000
characters long (including spaces).  Figure descriptions
should not repeat the figure caption – their purpose is to capture
important information that is not already provided in the caption or
the main text of the paper. For figures that convey important and
complex new information, a short text description may not be
adequate. More complex alternative descriptions can be placed in an
appendix and referenced in a short figure description. For example,
provide a data table capturing the information in a bar chart, or a
structured list representing a graph.  For additional information
regarding how best to write figure descriptions and why doing this is
so important, please see

§.§ The “Teaser Figure”

A “teaser figure” is an image, or set of images in one figure, that
are placed after all author and affiliation information, and before
the body of the article, spanning the page. If you wish to have such a
figure in your article, place the command immediately before the

§ CITATIONS AND BIBLIOGRAPHIES

The use of  for the preparation and formatting of one's
references is strongly recommended. Authors' names should be complete
— use full first names (“Donald E. Knuth”) not initials
(“D. E. Knuth”) — and the salient identifying features of a
reference should be included: title, year, volume, number, pages,
article DOI, etc.

The bibliography is included in your source document with these two
commands, placed just before the  command:

where “” is the name, without the “”
suffix, of the  file.

Citations and references are numbered by default. A small number of
ACM publications have citations and references formatted in the
“author year” style; for these exceptions, please include this
command in the preamble (before the command
“”) of your  source:

Some examples.  A paginated journal article <cit.>, an
enumerated journal article <cit.>, a reference to an entire
issue <cit.>, a monograph (whole book) <cit.>, a
monograph/whole book in a series (see 2a in spec. document)
<cit.>, a divisible-book such as an anthology or compilation
<cit.> followed by the same example, however we only output
the series if the volume number is given <cit.> (so
Editor00a's series should NOT be present since it has no vol. no.),
a chapter in a divisible book <cit.>, a chapter in a
divisible book in a series <cit.>, a multi-volume work as
book <cit.>, a couple of articles in a proceedings (of a
conference, symposium, workshop for example) (paginated proceedings
article) <cit.>, a proceedings article with
all possible elements <cit.>, an example of an enumerated
proceedings article <cit.>, an informally published work
<cit.>, a couple of preprints <cit.>, a doctoral dissertation <cit.>, a
master's thesis: <cit.>, an online document / world wide web
resource <cit.>, a video game
(Case 1) <cit.> and (Case 2) <cit.> and <cit.>
and (Case 3) a patent <cit.>, work accepted for
publication <cit.>, 'YYYYb'-test for prolific author
<cit.> and <cit.>. Other cites might
contain 'duplicate' DOI and URLs (some SIAM articles)
<cit.>. Boris / Barbara Beeton:
multi-volume works as books <cit.> and <cit.>. A
couple of citations with DOIs:
<cit.>. Online
citations: <cit.>.
Artifacts: <cit.> and <cit.>.

§ ACKNOWLEDGMENTS

Identification of funding sources and other support, and thanks to
individuals and groups that assisted in the research and the
preparation of the work should be included in an acknowledgment
section, which is placed just before the reference section in your

This section has a special environment:

so that the information contained therein can be more easily collected
during the article metadata extraction phase, and to ensure
consistency in the spelling of the section heading.

Authors should not prepare this section as a numbered or unnumbered ; please use the “” environment.

§ APPENDICES

If your work needs an appendix, add it before the
“” command at the conclusion of your source

Start the appendix with the “” command:

and note that in the appendix, sections are lettered, not
numbered. This document has two appendices, demonstrating the section
and subsection identification method.

§ MULTI-LANGUAGE PAPERS

Papers may be written in languages other than English or include
titles, subtitles, keywords and abstracts in different languages (as a
rule, a paper in a language other than English should include an
English title and an English abstract).  Use  for
every language used in the paper.  The last language indicated is the
main language of the paper.  For example, a French paper with
additional titles and abstracts in English and German may start with
the following command

The title, subtitle, keywords and abstract will be typeset in the main
language of the paper.  The commands ,
begin title, subtitle and keywords, can be used to set these elements
in the other languages.  The environment  is
used to set the translation of the abstract.  These commands and
environment have a mandatory first argument: the language of the
second argument.  See  file for examples
of their usage.

§ SIGCHI EXTENDED ABSTRACTS

The “” template style (available only in  and
not in Word) produces a landscape-orientation formatted article, with
a wide left margin. Three environments are available for use with the
“” template style, and produce formatted output in
the margin:

:  Place formatted text in the margin.

: Place a figure in the margin.

: Place a table in the margin.

To Robert, for the bagels and explaining CMYK and color spaces.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Abramsky et al(2000)]
authorpersonSamson Abramsky, personRadha
Jagadeesan, and personPasquale Malacaria.
Full Abstraction for PCF.
journalInf. Comput. volume163,
number2 (year2000), pages409–470.

[Castellan et al(2019)]
authorpersonSimon Castellan, personPierre
Clairambault, and personGlynn Winskel.
Thin Games with Symmetry and Concurrent Hyland-Ong
journalLog. Methods Comput. Sci.
volume15, number1 (year2019).

[Clairambault and Forest(2023)]
authorpersonPierre Clairambault and
personSimon Forest. year2023.
The Cartesian Closed Bicategory of Thin Spans of
Groupoids. In booktitleLICS. pages1–13.

[Clairambault et al(2023)]
authorpersonPierre Clairambault,
personFederico Olimpieri, and personHugo Paquet.
From Thin Concurrent Games to Generalized Species
of Structures. In booktitleLICS.

[De Carvalho(2007)]
authorpersonDaniel De Carvalho.
titleSémantiques de la logique linéaire et
temps de calcul.
thesistypePh. D. Dissertation.

[de Carvalho(2018)]
authorpersonDaniel de Carvalho.
Execution time of $\lambda$-terms via denotational
semantics and intersection types.
journalMath. Struct. Comput. Sci.
volume28, number7 (year2018),

[de Carvalho et al(2011)]
authorpersonDaniel de Carvalho,
personMichele Pagani, and personLorenzo Tortora de
Falco. year2011.
A semantic measure of the execution time in linear
journalTheor. Comput. Sci. volume412,
number20 (year2011), pages1884–1902.

authorpersonThomas Ehrhard.
On Köthe Sequence Spaces and Linear Logic.
journalMath. Struct. Comput. Sci.
volume12, number5 (year2002),

[Ehrhard et al(2018)]
authorpersonThomas Ehrhard, personMichele
Pagani, and personChristine Tasson.
Full Abstraction for Probabilistic PCF.
journalJ. ACM volume65,
number4 (year2018), pages23:1–23:44.

[Ehrhard and Regnier(2003)]
authorpersonThomas Ehrhard and
personLaurent Regnier. year2003.
The differential lambda-calculus.
journalTheor. Comput. Sci. volume309,
number1-3 (year2003), pages1–41.

[Ehrhard and Regnier(2008)]
authorpersonThomas Ehrhard and
personLaurent Regnier. year2008.
Uniformity and the Taylor expansion of ordinary
journalTheoretical Computer Science
volume403, number2-3 (year2008),

[Fiore et al(2008)]
authorpersonMarcelo Fiore, personNicola
Gambino, personMartin Hyland, and personGlynn
Winskel. year2008.
The cartesian closed bicategory of generalised
species of structures.
journalJournal of the London Mathematical Society
volume77, number1 (year2008),

[Fiore and Saville(2021)]
authorpersonMarcelo Fiore and personPhilip
Saville. year2021.
Coherence for bicategorical cartesian closed
journalMath. Struct. Comput. Sci.
volume31, number7 (year2021),

authorpersonPhilippa Gardner.
Discovering Needed Reductions Using Type Theory.
In booktitleTACS (seriesLecture Notes
in Computer Science, Vol. volume789).
publisherSpringer, pages555–574.

authorpersonJean-Yves Girard.
Linear Logic.
journalTheor. Comput. Sci.  volume50
(year1987), pages1–102.

authorpersonJean-Yves Girard.
Normal functors, power series and
journalAnn. Pure Appl. Log. volume37,
number2 (year1988), pages129–177.

[Hyland and Ong(2000)]
authorpersonJ. M. E. Hyland and
personC.-H. Luke Ong. year2000.
On Full Abstraction for PCF: I, II, and
journalInf. Comput. volume163,
number2 (year2000), pages285–408.

authorpersonMartin Hyland.
Game Semantics.
journalSemantics and Logics of Computation
volume14 (year1997), pages131.

[Laird et al(2013)]
authorpersonJim Laird, personGiulio
Manzonetto, personGuy McCusker, and personMichele
Pagani. year2013.
Weighted Relational Models of Typed
Lambda-Calculi. In booktitle28th Annual ACM/IEEE
Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA,
June 25-28, 2013. publisherIEEE Computer Society,

authorpersonFrançois Lamarche.
Quantitative Domains and Infinitary Algebras.
journalTheor. Comput. Sci. volume94,
number1 (year1992), pages37–62.

authorpersonPaul-André Melliès.
Template games and differential linear logic. In
booktitleLICS. publisherIEEE,

authorpersonPaul-André Mellies.
titleAsynchronous games 1: Uniformity by group

authorpersonPaul-André Mellies.
Categorical semantics of linear logic.
journalPanoramas et syntheses
volume27 (year2009), pages15–215.

authorpersonFederico Olimpieri.
Intersection Type Distributors. In
booktitle36th Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021.
publisherIEEE, pages1–15.

[Olimpieri and Auclair(2022)]
authorpersonFederico Olimpieri and
personLionel Vaux Auclair. year2022.
On the Taylor expansion of $\lambda$-terms and the
groupoid structure of their rigid approximants.
journalLog. Methods Comput. Sci.
volume18, number1 (year2022).

[Pagani et al(2014)]
authorpersonMichele Pagani, personPeter
Selinger, and personBenoît Valiron.
Applying quantitative semantics to higher-order
quantum computing. In booktitlePOPL.
publisherACM, pages647–658.

[Tsukada et al(2017)]
authorpersonTakeshi Tsukada, personKazuyuki
Asada, and personC.-H. Luke Ong.
Generalised species of rigid resource terms. In
booktitle32nd Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017.
publisherIEEE Computer Society, pages1–12.

[Tsukada et al(2018)]
authorpersonTakeshi Tsukada, personKazuyuki
Asada, and personC.-H. Luke Ong.
Species, Profunctors and Taylor Expansion Weighted
by SMCC: A Unified Framework for Modelling Nondeterministic,
Probabilistic and Quantum Programs. In booktitleLICS.
publisherACM, pages889–898.