Linear type systems need to keep track of how programs use their resources.
The standard approach is to use context splits specifying how resources are (disjointly) split across subterms.
In this approach, context splits redundantly echo information which is already present within subterms.  An alternative approach is to use leftover typing [24, 2], where in addition to the usual (input) usage context, typing judgments have also an output usage context: the leftovers.
In this approach, the leftovers of one typing derivation are fed as input to the next, threading through linear resources while avoiding context splits.
We use leftover typing to define a type system for a resource-aware  [28, 27], a process algebra used to  model concurrent systems.
Our type system is parametrised over a set of usage algebras [21, 35] that are general enough to encompass shared types (free to reuse and discard), graded types (use exactly $n$ number of times) and linear types (use exactly once).
Linear types are important in the : they ensure privacy and safety of communication and avoid race conditions, while graded and shared types allow for more flexible programming.
We provide a framing theorem for our type system, generalise the weakening and strengthening theorems to include linear types, and prove subject reduction.
Our formalisation is fully mechanised in about 1850 lines of Agda [37].

§ INTRODUCTION

The  [28, 27] is a computational model for communication and concurrency that boils concurrent processing down to the sending and receiving of data over communication channels.
Notably, it features channel mobility: channels themselves are first class values and can be sent and received.
Kobayashi et al. [23] introduced a typed version of the  with linear channel types, where channels must be used exactly once.
Linearity in the  guarantees privacy and safety of communication and avoids race conditions.

More broadly, linearity allows for resource-aware programming and more efficient implementations [36], and it  inspired unique types (as in Clean [4]), and ownership types (as in Rust [25]).
A linear type system must keep track of what resources are used in which parts of the program, and guarantee that they are neither duplicated nor discarded.
To do so, the standard approach is to use context splits: typing rules for terms with multiple subterms add an extra side condition specifying what resources to allocate to each of the subterms.
The typing derivations for the subterms must then use the entirety of their allocated resources.
A key observation here is that each subterm already knows about the resources it needs.
Context splits contain usage information that is already present in the subterms.
Moreover, the subterms cannot be typed until the context splits have been defined.
On top of that, using binary context splits means that typing rules with $n$ subterms require $n - 1$ context splits, which considerably clutters the type system.

An alternative approach is leftover typing, a technique used to formulate intuitionistic linear logic [24] and to mechanise the linear  [2].
Leftover typing changes the shape of the typing judgments and includes a second leftover output context that contains the resources that were left unused by the term.
As a result, typing rules thread the resources through subterms without needing context splits: each subterm uses the resources it needs, and leaves the rest for its siblings.
The first subterm in this chain of resources immediately knows what resources it has available.

In this paper, we use leftover typing to define for the first time a resource-aware type system for the , and we fully mechanise our work in Agda [37].
All previous work on mechanisation of linear process calculi uses context splits instead [16, 19, 17, 34, 8]. We will further highlight the benefits of leftover typing as opposed to context splits in contributions and the rest of the paper.

Below we present two alternative typing rules for parallel composition in the linear : the one on the left uses context splits, while the one on the right does not, and uses leftover typing instead:

Δ  ⊢   P
Ξ  ⊢   Q
Γ  ⊢   PQ

Γ  ⊢   P   ▹   Δ
Δ  ⊢   Q   ▹   Ξ
Γ  ⊢   PQ   ▹   Ξ

*Contributions and Structure of the Paper

* Leftover typing for resource-aware . Our type system uses leftover typing to model the resource-aware  (<ref>) and satisfies subject reduction (<ref>).
In addition to making context splits unnecessary, leftover typing allows for a framing theorem (<ref>) to be stated and is naturally associative, making type safety properties considerably easier to reason about (<ref>).
Thanks to leftover typing, we can now state weakening (<ref>) and strengthening (<ref>) for the whole framework, not just the shared fragment. This give a uniform and complete presentation of all the meta-theory for the resource-aware .

* Shared, graded and linear unified .
We generalise resource counting to a set of usage algebras that can be mixed within the same type system.
We do not instantiate our type system to only work with linear resources, instead we present an algebra-agnostic type system, and admit a mix of user-defined resource aware algebras [21, 35] (<ref>).
Any partial commutative monoid that is decidable, deterministic, cancellative and has a minimal element is a valid such algebra.
Multiple algebras can be mixed in the type system — usage contexts keep information about what algebra to use for each type (<ref>).
In particular, this allows for type systems combining linear (use exactly once), graded (exact number of $n$ times) and shared (free to reuse and discard) types under the same framework.

* Full mechanisation in Agda. The formalisation of the  with leftover typing, from the syntax to the semantics and the type system, has been fully mechanised in Agda in about 1850 lines of code, and is publicly available at [37].  We have fully mechanised all meta-theory and the details of a proof of subject reduction can be found in Appendix <ref>.

We use type level de Bruijn indices [12, 15] to define a syntax of  processes that is well scoped by construction: every free variable is accounted for in the type of the process that uses it (<ref>).
We then provide an operational semantics for the , prior to any typing (<ref>).
This operational semantics is defined as a reduction relation on processes.
The reduction relation tracks at the type level the channel on which communication occurs.
This information is later used to state the subject reduction theorem.
The reduction relation is defined modulo structural congruence — a relation defined on processes that acts as a quotient type to remove unnecessary syntactic minutiae introduced by the syntax of the .
We then define an interface for resource-aware algebras (<ref>) and use it to parametrise a type system based on leftover typing (<ref>).
Finally, we present the meta theoretical properties of our type system in <ref>.

Data type definitions ($\type{\N}$) use double inference lines and index-free synonyms (Nat) as rule names for ease of reference.
Constructors ($\constr{0}$ and $\suc$) are used as inference rule names.
We maintain a close correspondence between the definitions presented in this paper and our mechanised definitions in Agda: inference rules become type constructors, premises become argument types and conclusions return types.
Universe levels and universe polymorphism are omitted for brevity — all our types are of type $\Set$.
Implicit arguments are mentioned in type definitions but omitted by constructors.

0 :

n :
n :

We use colours to further distinguish the different entities in this paper.
$\type{TYPES}$ are blue and uppercased, with indices as subscripts, $\constr{constructors}$ are orange, $\func{functions}$ are teal, variables are black, and some constructor names are overloaded — and disambiguated by context.

§ SYNTAX

In order to mechanise the  syntax in Agda, we need to deal with bound names in continuation processes.
Names are cumbersome to mechanise: they are not inherently well scoped, one has to deal with alpha-conversion, and inserting new variables into a context entails proving that their names differ from all other names in context.
To overcome these challenges, we use de Bruijn indices [12], where a natural number $n$ (aka index) is used to refer to the variable introduced $n$ binders ago.
That is, binders no longer introduce names; terms at different depths use different indices to refer to the same binding.

While de Bruijn indices are useful for mechanisation, they are not as readable as names. To overcome this difficulty and demonstrate the correspondence between a  that uses names and one that uses de Bruijn indices,
we provide conversion functions in both directions and prove that they are inverses of each other up to $\alpha$-conversion. Further details can be found in Appendix <ref>.

[Var and Process]
A variable reference occurring under $n$ binders can refer to $n$ distinct variables.
We introduce the indexed family of types [15] $\Var_n$: for all naturals $n$, the type $\Var_n$ has $n$ distinct elements.
We index processes according to their depth: for all naturals $n$, a process of type $\Process_n$ contains free variables that can refer to $n$ distinct elements.
Every time we go under a binder, we increase the index of the continuation process, allowing the variable references within to refer to one more thing.

n :
_n :

n :
0 : _n

x : _n
x : _n

n :
_n :

\begin{equation*}
\begin{aligned}
\Process_n ::=& \; \PO                &&\text{(inaction)}   \\
|& \; \new{} \Process_{\suc n}         &&\text{(restriction)}          \\
|& \; \comp{\Process_n}{\Process_n}    &&\text{(parallel)} \\
|& \; \recv{\Var_n}{}\Process_{\suc n} &&\text{(input)}                \\
|& \; \send{\Var_n}{\Var_n}\Process_n  &&\text{(output)}
\end{aligned}
\end{equation*}

Process $\PO$ denotes the terminated process, where no further communications can occur;
process $\new{} P$ creates a new channel and binds it at index $0$ in the continuation process $P$;
process $\comp{P}{Q}$ composes $P$ and $Q$ in parallel;
process $\recv{x}{}P$ receives data along channel $x$ and makes that data available at index $0$ in the continuation process $P$;
process $\send{x}{y}{P}$ sends variable $y$ over channel $x$ and continues as process $P$.

[The courier system]

We present a courier system that consists of three roles:
a sender, who wants to send a package;
a receiver, who receives the package sent by the sender;
and a courier, who carries the package from the sender to the receiver.

[draw,circle,fill opacity=0.3,text opacity=1,fill=brown] (send-x) at (0,2)   $\func{send} \, x$;
[draw,circle,fill opacity=0.3,text opacity=1,fill=brown] (send-y) at (0,0)   $\func{send} \, y$;
[draw,circle,fill opacity=0.3,text opacity=1,fill=purple] (recv-z) at (4,1)   $\func{recv} \, z$;
[draw,circle,fill opacity=0.3,text opacity=1,fill=cyan,align=center] (sync) at (2,1)   $\func{carry}$
$ \, x \, y \, z$;

[->] (send-x) – node[above] $x$ (sync);
[->] (send-y) – node[below] $y$ (sync);
[->] (sync.10) – node[above] $z$ (recv-z.170);
[->] (sync) – (recv-z);

Our courier system is defined by four  processes composed in parallel instantiating the above three roles:
we have two sender processes, $\func{send} \, x$ and $\func{send} \, y$, sending data over channels $x$ and $y$, respectively;
one receiver process, $\func{recv} \, z$, which receives over channel $z$ the data sent from each of the senders – hence receives twice;
and a courier process $\func{carry} \, x \, y \, z$, which synchronises communication among the senders and the receiver.
The courier process first receives data from the two senders along its input channels $x$ and $y$, and then sends the two received bits of data to the receiver along its output channel $z$.

The sender and receiver roles are defined below, parametrised by the channels on which they operate.
The sender creates a new channel to be sent as data, and sends it over channel $c$, and then terminates.
Processes $\func{send} \, x$ and $\func{send} \, y$ are an instantiation of $\func{send} \, c$.
The receiver receives data twice on a channel $c$ and then terminates.
The receiver process $\func{recv} \, z$ is an instantiation of $\func{recv} \, c$.

\begin{align*}
& \func{send} \; c = \new{} (\send{\suc c}{\constr{0}} \PO) &&
\func{recv} \; c \; = \recv{c}{} \recv{(\suc c)}{} \PO
\end{align*}

The courier role is defined below as $\func{carry} \; x \; y \; z$.
It sequentially receives on the two input channels $x$ and $y$, instantiated as $in0$ and $in1$, and then outputs the two pieces of received data on the output channel $z$, instantiated as $out$.
Finally, we create three communication channels and compose all four processes together: the first channel is shared between the one sender and the courier, the second between the other sender and the courier, and the third between the receiver  and the courier.
The result is the courier $\func{system}$ defined below.

\begin{align*}
& \func{carry} \; in0 \; in1 \; out \; =  \recv{in0 }{}
\recv{(\suc \; in1) }{}
\send{(\suc \suc \; out) }{\suc \constr{0}}
\send{(\suc \suc \; out) }{\constr{0}} \PO \\
& \func{system} =  \new{} ( \func{send} \; \constr{0}
\comp{}{\new{} ( \func{send} \; \constr{0} }
\comp{}{\new{} ( \func{recv} \; \constr{0} }
\comp{}{\func{carry} \; (\suc \suc \constr{0}) \; (\suc \constr{0}) \; \constr{0}))) }
\end{align*}

We continue this running example in  <ref>, where we provide typing derivations for the above processes and use a mix of linear, graded and shared typing to type the courier $\func{system}$.

§ OPERATIONAL SEMANTICS

Thanks to our well-scoped grammar in <ref>, we now define the semantics of our language on the totality of the syntax.

We consider a variable $i$ to be unused in $P$ ($\Unused_i \; P$) if none of the inputs nor the outputs refer to it.
$\Unused_i \; P$ is defined as a recursive predicate on $P$, incrementing $i$ every time we go under a binder, and using $i \type{\not\equiv} x$ ( which unfolds to the negation of propositional equality on Var, i.e. $i \type{\equiv} x \to \type{\bot}$) to compare variables.

We define the base cases of a structural congruence relation $\eqeq$ as follows:

P Q :

comp-assoc : P(QR) (PQ)R

comp-sym : PQ QP

comp-id : P_n P

scope-end : _n _n

uQ : _0   Q
scope-ext : (PQ) (P)lower_0     Q   uQ

scope-comm : P exchange_0   P

The first three rules ($\constr{comp}-$*) state associativity, symmetry, and $\PO$ as being the neutral element of parallel composition, respectively.
The last three ($\constr{scope}-$*) state garbage collection, scope extrusion and commutativity of restrictions, respectively.
In $\constr{scope-ext}$ the side condition $\Unused_i \; Q$ makes sure that $i$ is unused in $Q$ (see <ref>).
The function $\func{lower}_i \; Q \; uQ$ traverses $Q$ decrementing every index greater than $i$.
In $\constr{scope-comm}$ the function $\func{exchange}_i \; P$ traverses $P$ (of type $\allowbreak \Process_{\suc \suc n}$) and swaps variable references $i$ and $\suc i$.
In all the above, $i$ is incremented every time we go under a binder.

We lift the relation StructCong $\eqeq{}$ and close it under equivalence and congruence in $\eq{}$.
This relation is structurally congruent under a context $\mathcal{C}[\cdot]$ [32] and is reflexive, symmetric and transitive.

The operational semantics of the  is defined as a reduction relation $\reduce{c}$ indexed by the channel $c$ on which communication occurs.
We keep track of channel $c$ so we can state subject reduction (<ref>).

n :
_n :

internal : _n

i : _n
external   i : _n

c : _n
P   Q : _n
P c Q :

i   j : _n
P : _n
Q : _n
comm : iPijQ external   i lower_0   (Pj0)   uP'Q

red : P c P'
par   red : PQ c P'Q

red : P c Q
res   red : P dec  c Q

eq_1 : P  P'
red : P' c Q'
eq_2 : Q'  Q
struct   eq   red : P c Q

We distinguish between channels that are created inside the process ($\constr{internal}$), and channels that are created outside ($\constr{external}\ i$), where $i$ is the index of the channel variable.
In rule $\constr{comm}$, parallel processes reduce when they communicate over a common channel with index ${i}$.
As a result of that communication, the continuation of the input process $P$ has all the references to its most immediate variable substituted with references to $\suc j$, the variable sent by the output process $\send{i}{j}{Q}$.
After this substitution, $\subst{P}{\suc j}{\constr{0}}$ is lowered — all variable references are decreased by one (and we derive the proof $\Unused_{\constr{0}} \; (\subst{P}{\suc j}{\constr{0}})$).
Reduction is closed under parallel composition (rule $\constr{par}$), restriction (rule $\constr{res}$) and structural congruence (rule $\constr{struct}$)
— notably, not under input nor output, as doing so would not preserve the sequencing of actions [32].
Rule $\constr{res}$ uses $\func{dec}$ to decrement the index of channel $c$ as we wrap processes $P$ and $Q$ inside a binder.
It is defined as expected below:

\begin{equation*}
\begin{aligned}
& \func{dec} \; \constr{internal}                 && = \constr{internal} \\
& \func{dec} \; (\constr{external} \; \constr{0}) && = \constr{internal} \\
& \func{dec} \; (\constr{external} \; (\suc n))   && = \constr{external} \; n \\
\end{aligned}
\end{equation*}

§ RESOURCE-AWARE TYPE SYSTEM

In <ref> we characterise a usage algebra for our type system.
It defines how resources are split in parallel composition and consumed in input and output.
We define typing and usage contexts in <ref>.
We provide a type system for a resource-aware  in <ref>.

§.§ Multiplicities and Capabilities

In the linear  each channel has an input and an output capability, and each capability has a given multiplicity of 0 (exhausted) or 1 (available).
We generalise over this notion by defining an algebra for multiplicities [21, 35] that is satisfied by linear, graded and shared types alike.
We then use pairs of multiplicities as usage annotations for a channel's input and output capabilities.

A usage algebra is a ternary relation $\op{x}{y}{z}$ that is partial (as not any two multiplicities can be combined), deterministic and cancellative (to aid equational reasoning) and associative and commutative (following directly from subject congruence for parallel composition).
In addition, we ask that the leftovers can be computed so that we can automatically update the usage context every time input and output occurs — this is purely for usability.
It has a neutral element $\zero$ that is absorbed on either side, and that is also minimal (so that new resources cannot arbitrarily spring into life).
It has an element $\one$ that is used to count inputs and outputs.
Below we define such an algebra as a record $\Algebra_C$ on a carrier $C$.
(We use $\forall$ for universal quantification.
The dependent product $\type{\exists}$ uses the value of its first argument in the type of its second.
The type $\type{DEC} \; P$ is a witness of either $P$ or $P \to \type{\bot}$, where $\type{\bot}$ is the empty type with no constructors.)

\begin{equation*}
\begin{aligned}
&\op{\_}{\_}{\_}         &:{} &                 &        & C \to C \to C \to \Set \\
&\func{\cdot-unique}     &:{} &\forall x x' y z  & \to \; & \op{x'}{y}{z} \to \op{x}{y}{z} \to x' \equiv x \\
&\func{\cdot-unique^l}   &:{} &\forall x y y' z  & \to \; & \op{x}{y'}{z} \to \op{x}{y}{z} \to y' \equiv y \\
&\func{\cdot-assoc}      &:{} &\forall x y z u v & \to \; & \op{x}{y}{z} \to \op{y}{u}{v} \to \type{\exists} w  \; (\op{x}{u}{w} \times \op{w}{v}{z}) \\
&\func{\cdot-comm}       &:{} &\forall x y z     & \to \; & \op{x}{y}{z} \to \op{x}{z}{y} \\
&\func{\cdot-compute^r}  &:{} &\forall x y       & \to \; & \type{DEC} \; (\type{\exists} z  \; (\op{x}{y}{z})) \\
&\zero                   &:{} &                 &        & C \\
&\func{\cdot-id^l}       &:{} &\forall x         & \to \; & \op{x}{\zero}{x} \\
&\func{\cdot-min^l}      &:{} &\forall y z        & \to \; & \op{\zero}{y}{z} \to y \equiv \zero \\
&\one                    &:{} &                 &        & C \\
\end{aligned}
\end{equation*}

We sketch the implementation of linear, graded and shared types as instances of our usage algebra below.
Their use in typing derivations is illustrated in <ref>.

carrier     operation

linear     [cl]$\constr{0} \, : \, \type{Lin}$
$\constr{1} \, : \, \type{Lin}$     [cl]$\op{\constr{0}}{\constr{0}}{\constr{0}}$

graded     [cl]$\constr{0} \, : \type{Gra}$
$\suc \, : \type{Gra} \to \type{Gra}$     [cl]$\forall \, x \, y \, z$
$\to x \, \type{\equiv} \, y \, \func{+} \, z$
$\to \op{x}{y}{z}$

shared     $\constr{\omega} \, : \, \type{Sha}$     $\op{\constr{\omega}}{\constr{\omega}}{\constr{\omega}}$

§.§ Typing Contexts

We use indexed sets of usage algebras to allow several usage algebras to coexist in our type system with leftovers (<ref>).
An indexed set of usage algebras is a type $\Idx$ of indices that is nonempty ($\type{\exists IDX}$) together with an interpretation $\Usage$ of indices into types, and an interpretation $\type{ALGEBRAS}$ of indices into usage algebras of the corresponding type.

\begin{equation*}
\begin{aligned}
&\Idx               &:{} &\Set \\
&\type{\exists IDX} &:{} &\Idx \\
&\Usage             &:{} &\Idx \to \Set \\
&\type{ALGEBRAS}    &:{} &(idx : \Idx) \to \Algebra_{\Usage_{idx}}
\end{aligned}
\end{equation*}

We keep typing contexts ($\PreCtx$) and usage contexts ($\Ctx$) separate.
The former are preserved throughout typing derivations; the latter are transformed as a result of input, output, and context splits.
[Type and PreCtx: types and typing contexts]
A type is either a unit type ($\unit$),

or a channel type ($\channel{t}{x}$).

t :
idx :

x : _idx^2
tx :

The unit type $\unit$ serves as a base case for types.

The type $\channel{t}{x}$ of a channel determines what type ${t}$ of data and what usage annotations ${x}$ are sent over that channel — we use the notation $\type{C}^{\func{2}}$ to stand for a $\type{C} \constr{\times} \type{C}$ pair of input and output multiplicities, respectively.
This channel notation aligns with $[t]\ \mathbf{chan}_{(i^{y},o^{z})}$, where $y,z$ are the input and output multiplicities, respectively [22].
Henceforth, we use $\lz$ to denote the multiplicity pair $\zero \comma \zero$, $\li$ for the pair $\one \comma \zero$, $\lo$ for $\zero \comma \one$, and $\lio$ for $\one \comma \one$.
This notation was originally used in the linear  [23, 32].
A typing context $\PreCtx_n$ is a length-indexed list of types that is either empty ($\constr{[]}$) or the result of appending a type $t : \Type$ to an existing context ($\gamma \constr{,} t$).

[Idxs and Ctx: contexts of indices and usage contexts]
A context of indices $\Idxs_n$ is a length-indexed list that is either empty ($\constr{[]}$) or the result of appending an index $i : \Idx$ to an existing context ($idxs \constr{,} i$).
A usage context is a context $\Ctx_{idxs}$ indexed by a context of indices $idxs : \Idxs_n$ that is either empty ($\constr{[]}$) or the result or appending a usage annotation pair $u : \Usage_{idx}^{\func{2}}$ with index $idx : \Idx$ to an existing context ($\Gamma \constr{,} u$).

§.§ Typing with Leftovers

We present a resource-aware type system for the  based on leftover typing [2], a technique that, in addition to the usual typing context $\PreCtx_n$ and (input) usage context $\Ctx_{idxs}$, adds an extra (output) usage context $\Ctx_{idxs}$ to the typing rules.
This output context contains the leftovers (the unused multiplicities) of the process being typed.
These leftovers can then be used as input to another typing derivation.

Leftover typing inverts the information flow of usage annotations so that it is the typing derivations of subprocesses which determine how resources are allocated.
As a result, context split proofs are no longer necessary.
Leftover typing also allows framing to be stated, and weakening and strengthening to cover linear types too.

Our type system is composed of two typing judgments: one for variable references (<ref>) and one for processes (<ref>).
Both judgments are indexed by a typing context $\gamma$, an input usage context $\Gamma$, and an output usage context $\Delta$ (the leftovers).
The typing judgement for variables $\contains{\gamma}{\Gamma}{i}{t}{y}{\Delta}$ asserts that “index $i$ in typing context $\gamma$ is of type $t$, and subtracting $y$ at position $i$ from input usage context $\Gamma$ results in leftovers $\Delta$”.
The typing judgement for processes $\types{\gamma}{\Gamma}{P}{\Delta}$ asserts that “process $P$ is well typed under typing context $\gamma$, usage input context $\Gamma$ and leftovers $\Delta$”.

[VarRef: typing variable references]
The VarRef typing relation for variable references is presented below.

γ: _n

i : _n

t :

idx :

y : _idx^2

idxs : _n

Γ  Δ: _idxs
γΓityΔ :

0 : γtΓx0tyΓz

v : γΓitxΔ
v : γt'Γx'itxΔx'

We lift the operation $\op{x}{y}{z}$ and its algebraic properties to an operation $\opsquared{(x_l \comma x_r)}{(y_l \comma y_r)}{(z_l \comma z_r)}$ on pairs of multiplicities.
The base case $\constr{0}$ splits the usage annotation $x$ of type $\Usage_{idx}^{\func{2}}$ into $y$ and $z$ (the leftovers).
Note that the remaining context $\Gamma$ is preserved unused as a leftover.
This splitting $\opsquared{x}{y}{z}$ is as per the usage algebra provided by the developer for the index $idx$.
In our Agda implementation, $\opsquared{x}{y}{z}$ is actually a trivially satisfiable implicit argument if $\opsquared{x}{y}{z}$ is inhabited and an unsatisfiable argument otherwise.
The inductive case $\suc$ appends the type $t'$ to the typing context, and the usage annotation $x'$ to both the input and output usage contexts.

[Variable reference]
$\func{egVar}$ defines a variable reference $\suc \constr{0}$ with type $\channel{\unit}{\li}$ and usage $\li$.
We must show that this variable is well typed in an environment with a typing context $\gamma = \constr{[]} \comma \channel{\unit}{\li} \comma \unit$ and a usage context $\Gamma = \constr{[]} \comma \lio \comma \lio$.
The VarRef constructors are completely determined by the variable index $\suc \; \constr{0}$ in the type.
The constructor $\suc$ steps under the outermost variable in the context, preserving its usage annotation $\lio$ from input to output.
The constructor $\constr{0}$ asserts that the next variable is of type $\channel{\unit}{\li}$, and that the usage annotation $\lio$ can be split such that $\op{\lio}{\li}{\lo}$ — using $\func{\cdot-compute^r}$ to automatically fulfill the proof obligation.

egVar   :   ([]  ) ([] ) 0   ([] )

egVar   =   0

[Types: typing processes]
The Types typing relation for the resource-aware  processes is presented below.
For convenience, we reuse the constructor names introduced for the syntax in <ref>.

γ: _n

P : _n

idxs : _n

Γ  Δ: _idxs
γΓPΔ :

: γΓΓ

t :
x : _idx^2
y : _idx'

cont : γtxΓ(y y) PΔ
t   x   y   cont : γΓPΔ

chan : γΓitxΞ

cont  : γtΞxP Θ
chan cont : γΓiPΘ

chan : γΓitxΔ

loc  : γΔjt x Ξ

cont  : γΞPΘ
chanloc cont : γΓijPΘ

l : γΓPΔ

r : γΔQΞ
lr : γΓPQΞ

The inaction process in rule $\PO$ does not change usage annotations.
The scope restriction in rule $\new$ expects three arguments: the type $t$ of data being transmitted; the usage annotation $x$ of what is being transmitted; and the multiplicity $y$ given to the channel itself.
This multiplicity $y$ is used for both input and output, so that they are balanced.
The continuation process $P$ is provided with the new channel with usage annotation $y \comma y$, which it must completely exhaust.

The input process in rule $\recv{}{}$ requires a channel $chan$ at index $i$ with usage $\li$ available, such that data with type $t$ and usage $x$ can be sent over it.
Note that the index $i$ is determined by the syntax of the typed process.
We use the leftovers $\Xi$ to type the continuation process, which is also provided with the received element — of type $t$ and multiplicity $x$ — at index $\constr{0}$.
The received element $x$ must be completely exhausted by the continuation process.

Similarly to input, the output process in rule $\send{}{}$ requires a channel $chan$ at index $i$ with usage $\lo$ available, such that data with type $t$ and usage $x$ can be sent over it.
We use the leftover context $\Delta$ to type the transmitted data, which needs an element $loc$ at index $j$ with type $t$ and usage $x$, as per the type of the channel $chan$.
The leftovers $\Xi$ are used to type the continuation process.
Note that both indices $i$ and $j$ are determined by the syntax of the typed process.

Parallel composition in rule $\comp{}{}$ uses the leftovers of the left-hand process to type the right-hand process.
Indeed, <ref> shows that an alternative rule where the resources are first threaded through $Q$ is admissible too.

[Typing derivation (Continued)]

We provide the typing derivation for the courier system defined in <ref>.
For the sake of simplicity, we instantiate these processes with concrete variable references before typing them.

The receiver defined by the $\func{recv}$ process receives data along the channel with index $\constr{0}$, which needs to be of type $\channel{t}{u}$ for some $t$ and $u$.
After receiving twice, the process ends: we must not be left with any unused multiplicities, thus $u = \lz$.
We will use graded types to keep track of the exact number of times communication happens.
Whatever the input multiplicity of the channel, we will consume $2$ of it and leave the remaining as leftovers.
The sender defined by the $\func{send}$ process sends data along the channel with index $\constr{0}$, which needs to be of type $\channel{t}{u}$ for some $t$ and $u$.
We instantiate $t$ (the type of data that the sender sends) to the trivial channel $\channel{\unit}{\func{\omega}}$.
As per the type of the process $\func{recv}$, $u = \lz$.
We will transmit once, thus use $\suc{\constr{0}}$ output multiplicity, and leave the rest as leftovers.
Agda can uniquely determine the arguments required by the $\new{}$ constructor.

\begin{align*}
& \func{recvwt} \;  : \; \types{\gamma \comma \channel{t}{\lz}  }{\Gamma \comma (\suc \suc l \comma r)  }{\func{recv} \; \constr{0}  }{\Gamma \comma (l \comma r)} \\
& \func{recvwt} \;  = \; \recv{\constr{0}}{} \recv{(\suc \constr{0})}{} \PO \\
& \func{sendwt} \;  : \; \types{\gamma \comma \channel{\channel{\unit}{\func{\omega}}}{\lz}  }{\Gamma \comma (l \comma \suc r)  }{\func{send} \; \constr{0}  }{\Gamma \comma (l \comma r)}  \\
& \func{sendwt} \;  = \; \new{} \; \_ \; \_ \; \zero \; (\send{\suc \constr{0}}{\constr{0}} \PO)
\end{align*}

Dually, the courier defined by the $\func{carry}$ process expects input multiplicities for the channels shared with $\func{send}$ and output multiplicities for the channel shared with $\func{recv}$.
We can now compose these processes in parallel and type the courier $\func{system}$.

\begin{align*}
& \func{carrywt} && : \types{\gamma \comma \channel{t}{\lz} \comma \channel{t}{\lz} \comma \channel{t}{\lz}\\ & &&}{\Gamma \comma (\suc lx \comma rx) \comma (\suc ly \comma ry) \comma (lz \comma \suc \suc rz)\\ & &&}{\func{carry} \; (\suc \suc \constr{0}) \; (\suc \constr{0}) \; \constr{0}\\ & &&}{\Gamma \comma (lx \comma rx) \comma (ly \comma ry) \comma (lz \comma rz)} & \\
& \func{carrywt} && = \recv{(\suc \suc \constr{0})}{} \recv{(\suc \suc \constr{0})}{} \send{(\suc \suc \constr{0})}{\suc \constr{0}} \send{(\suc \suc \constr{0})}{\constr{0}} \PO \\
& \func{systemwt} && : \; \types{\constr{[]}}{\constr{[]}}{\func{system}}{\constr{[]}} \\
& \func{systemwt} && = \new{} \; \_ \; \_ \; \_ \; ( \func{sendwt} \comp{}{ \new{} \; \_ \; \_ \; \_ } \; ( \func{sendwt} \comp{}{ \new{} \; \_ \; \_ \; \_ } \; ( \func{recvwt} \comp{}{ \func{carrywt} })))
\end{align*}

§ META-THEORY

We have mechanised subject reduction for our  with leftovers in 850 lines of Agda code.
The meta-theory of resource-aware type systems often needs to reason on typing derivations modulo associativity in the allocation of resources.
For type systems using context splitting side conditions, this means applying associativity lemmas to recompute context splits; for type systems using leftover typing it does not.
As an example, the proof that $\constr{comp-asssoc}$ preserves typing proceeds by deconstructing the input derivation into $\comp{P}{(\comp{Q}{R})}$ and reassembling it as $\comp{(\comp{P}{Q})}{R}$ without the need of any extra reasoning.

All the reasoning carried out in our type safety proofs is based on the algebraic properties introduced in <ref> – the exception to this is $\func{\cdot -compute^r}$, only there for the user's convenience.
We lift the operation $\opsquared{x}{y}{z}$ and its algebraic properties to an operation $\opctx{\Gamma}{\Delta}{\Xi}$ on usage contexts that have the same underlying context of indices.
The algebraic properties of the algebras allow us to see a typing derivation $\types{\gamma}{\Gamma}{P}{\Delta}$ as a unique arrow from $\Gamma$ to $\Delta$, and to freely compose and reason with arrows with the same typing context and a matching output and input usage contexts.

Leftover typing also allows us to state a framing theorem showing that adding or subtracting arbitrary usage annotations to the input and output usage contexts preserves typing – one can understand a typing derivation independently from its unused resources.
With framing one can show that $\constr{comp-comm}$ preserves typing: in $\comp{P}{Q}$ the typing of $P$ and $Q$ is independent of one another.

Let $\types{\gamma}{\Gamma_l}{P}{\Xi_l}$.
Let $\Delta$ be such that $\opctx{\Gamma_l}{\Delta}{\Xi_l}$.
Then for any $\Gamma_r$ and $\Xi_r$ where $\opctx{\Gamma_r}{\Delta}{\Xi_r}$ it holds that $\types{\gamma}{\Gamma_r}{P}{\Xi_r}$.

Leftover typing allows weakening and strengthening to acquire a more general form where linear variables can freely be added or removed from context too – as long as they are added and removed to and from both the input and output contexts.

Let $\func{ins}_i$ insert an element into a context at position $i$.
Let $P$ be well typed in $\types{\gamma}{\Gamma}{P}{\Xi}$.
Then, lifting every variable greater than or equal to $i$ in $P$ is well typed in
$\types{\func{ins}_i \; t \; \gamma}{\func{ins}_i \; x \; \Gamma}{\func{lift}_i \; P}{\func{ins}_i \; x \; \Xi}$.

Let $\func{del}_i$ delete the element at position $i$ from a context.
Let $P$ be well typed in $\types{\gamma}{\Gamma}{P}{\Xi}$.
Let $i$ be a variable not in $P$, such that $uP \; : \; \Unused_i \; P$.
Then lowering every variable greater than $i$ in $P$ is well typed in $\types{\func{del}_i \; \gamma}{\func{del}_i \; \Gamma}{\func{lower}_i \; P \; uP}{\func{del}_i \; \Xi}$.

Subject congruence states that structural congruence (<ref>) preserves the well-typedness of a process.
[Subject Congruence]

Let $P$ and $Q$ be processes. If $P \eq{} Q$ and $\types{\gamma}{\Gamma}{P}{\Xi}$, then $\types{\gamma}{\Gamma}{Q}{\Xi}$.

Finally, subject reduction states that reducing on a channel $c$ (<ref>) preserves the well-typedness of a process — after consuming $\lio$ from $c$ if $c$ is an $\constr{external}$ channel.  Below we use $\containsusage{\Gamma}{i}{x}{\Delta}$ to stand for $\contains{\gamma}{\Gamma}{i}{t}{x}{\Delta}$ for some $\gamma$ and $t$.
[Subject Reduction]

Let $\types{\gamma}{\Gamma}{P}{\Xi}$ and $P \reduce{c} Q$.
If $c$ is $\constr{internal}$, then $\types{\gamma}{\Gamma}{Q}{\Xi}$.
If $c$ is $\constr{external} \; i$ and $\containsusage{\Gamma}{i}{\lio}{\Delta}$, then $\types{\gamma}{\Delta}{Q}{\Xi}$.

We refer to Appendix <ref> for a more detailed account of the mechanised proofs.

§ CONCLUSIONS, RELATED AND FUTURE WORK

*Extrinsic Encodings

Extrinsic encodings define a syntax (often well-scoped) and a runtime semantics prior to any type system.
This allows one to talk about ill-typed terms, and defers the proof of subject reduction to a later stage.

To the best of our knowledge, leftover typing makes its appearance in 1994, when Ian Mackie first uses it to formulate intuitionistic linear logic [24].
Allais [2] uses leftover typing to mechanise in Agda a bidirectional type system for the linear .
He proves type preservation and provides a decision procedure for type checking and type inference.
In this paper, we follow Allais [2] and apply leftover typing to the  for the first time.
We generalise the usage algebra, leading to linear, graded and shared type systems.
Drawing from quantitative type theory (by McBride and Atkey [26, 3]), in our work we too are able to talk about fully consumed resources — e.g., we can transmit $\lz$ multiplicities of a fully exhausted channel.

Recent years have seen an increase in the efforts to mechanise resource-aware process algebras, but one of the earliest works is the mechanisation of the linear  in Isabelle/HOL by Gay [16].
Gay encodes the  with linear and shared types using de Bruijn indices, a reduction relation and a type system posterior to the syntax.
However, in his work typing rules demand user-provided context splits, and variables with consumed usage annotations are erased from context.
We remove the demand for context splits, preserve the ability to talk about consumed resources, and adopt a more general usage algebra.

Orchard et al. introduce Granule [29], a fully-fledged functional language with graded modal types, linear types, indexed types and polymorphism.
Modalities include exact usages, security levels and intervals; resource algebras are pre-ordered semirings with partial addition.
The authors provide bidirectional typing rules, and show the type safety of their semantics.

The work by Goto et al. [19] is, to the best of our knowledge, the first formalisation of session types which comes along with a mechanised proof of type safety in Coq.
The authors extend session types with polymorphism and pattern matching.
They use a locally-nameless encoding for variable references, a syntax prior to types, and an LTS semantics that encodes session-typed processes into the .
Their type system uses reordering of contexts and extrinsic context splits, which are not needed in our work.

*Intrinsic Encodings

Intrinsic encodings merge syntax and type system.
As a result, one can only ever talk about well-typed terms, and the reduction relation by construction carries a proof of subject reduction.
Significantly, by merging the syntax and static semantics of the object language one can fully use the expressive power of the host language.

Thiemann formalises in Agda the MicroSession (minimal GV [17]) calculus with support for recursion and subtyping [34].
As Gay does in [16], context splits are given extrinsically, and exhausted resources are removed from typing contexts altogether.
The runtime semantics are given as an intrinsically typed CEK machine with a global context of session-typed channels.

In their recent paper, Ciccone and Padovani mechanise a dependently-typed linear  in Agda [8].
Their intrinsic encoding allows them to leverage Agda's dependent types to provide a dependently-typed interpretation of messages — to avoid linearity violations the interpretation of channel types is erased.
Message input is modeled as a dependent function in Agda, and as a result message predicates, branching, and variable-length conversations can be encoded.
In contrast to our work, their algebra is on the multiplicities $0$, $1$, $\omega$, and top-down context splitting proofs must be provided.

In another recent work, Rouvoet et al. provide an intrinsic type system for a  with session types [31].
They use proof relevant separation logic and a notion of a supply and demand market to make context splits transparent to the user.
Their separation logic is based on a partial commutative monoid that need not be deterministic nor cancellative.
Their typing rules preserve the balance between supply and demand, and are extremely elegant.
They distill their typing rules even further by modelling the supply and demand market as a state monad.

*Other Work

Castro et al. [6] provide tooling for locally-nameless representations of process calculi in Coq, where de Bruijn indices are less popular than in Agda or Idris.
They use their tool to help automate proofs of subject reduction for a type system with session types.

Orchard and Yoshida [30] embed a small effecftul imperative language into the session-typed , showing that session types are expressive enough to encode effect systems.

Based on contextual type theory, LINCX [18] extends the linear logical framework LLF [7] by internalising the notion of bindings and contexts.
The result is a meta-theory in which HOAS encodings with both linear and dependent types can be described.
The developer obtains for free an equational theory of substitution and decidable typechecking without having to encode context splits within the object language.

Further work on mechanisation of the  [13, 20, 5, 14, 1], focuses on non-linear variations, differently from our range of linear, graded and shared types.

*Conclusions and Future Work

We provide a well-scoped syntax and a semantics for the , extrinsically define a type system on top of the syntax capable of handling linear, graded and shared types under the same unified framework and show subject reduction.
We avoid extrinsic context splits by defining a type system based on leftover typing [2].
As a result, theorems like framing, weakening and strengthening can now be stated also for the linear .
Our work is fully mechanised in around 1850 lines of code in Agda [37].

As future work we intend to expand our framework to include infinite behaviour by adding process replication, which is challenging, as to prove subject congruence one needs to uniquely determine the resources consumed by a process — e.g., by adding type annotations to the syntax.
Orthogonally, we aim to investigate making our typing rules bidirectional which would allow us to provide a decision procedure for type checking processes in a given set of algebras.
Finally, we will use our  with leftovers as an underlying framework on top of which we can implement session types, via their encodings into linear types [9, 11, 33] and other advanced type theories.

We want to thank Erika Kreuter, Wen Kokke, James Wood, Guillaume Allais, Bob Atkey, and Conor McBride for their valuable suggestions.

[1]
Affeldt, R., Kobayashi, N.: A Coq Library for Verification of Concurrent
Programs. Electron. Notes Theor. Comput. Sci.  199,  17–32 (2008).

[2]
Allais, G.: Typing with Leftovers - A mechanization of Intuitionistic
Multiplicative-Additive Linear Logic. In: Types for Proofs and Programs,
TYPES. LIPIcs, vol. 104, pp. 1:1–1:22. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik (2017). 10.4230/LIPIcs.TYPES.2017.1

[3]
Atkey, R.: Syntax and Semantics of Quantitative Type Theory. In: Logic in
Computer Science, LICS. pp. 56–65. ACM (2018).

[4]
Barendsen, E., Smetsers, S.: Uniqueness Typing for Functional Languages with
Graph Rewriting Semantics. Math. Struct. Comput. Sci.  6(6),
579–612 (1996)

[5]
Bengtson, J.: The pi-calculus in nominal logic, vol. 2012 (2012),

[6]
Castro, D., Ferreira, F., Yoshida, N.: EMTST: Engineering the Meta-theory of
Session Types. In: Tools and Algorithms for the Construction and Analysis of
Systems, TACAS. Lecture Notes in Computer Science, vol. 12079, pp.
278–285. Springer (2020). 10.1007/978-3-030-45237-7_17

[7]
Cervesato, I., Pfenning, F.: A Linear Logical Framework. In: Logic in
Computer Science, LICS. pp. 264–275. IEEE Computer Society (1996).

[8]
Ciccone, L., Padovani, L.: A Dependently Typed Linear \(\pi\)-Calculus in
Agda. In: PPDP '20: 22nd International Symposium on Principles and
Practice of Declarative Programming. pp. 8:1–8:14. ACM (2020).

[9]
Dardha, O.: Recursive Session Types Revisited. In: Carbone, M. (ed.) Workshop
on Behavioural Types, BEAT. EPTCS, vol. 162, pp. 27–34 (2014).

[10]
Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. In:
Principles and Practice of Declarative Programming, PPDP. pp. 139–150.
ACM (2012). 10.1145/2370776.2370794

[11]
Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. Inf.
Comput.  256,  253–286 (2017). 10.1016/j.ic.2017.06.002,
extended version of [10]

[12]
de Bruijn, N.G.: Lambda Calculus Notation with Nameless Dummies, a Tool for
Automatic Formula Manipulation, with Application to the Church-Rosser
Theorem. In: Indagationes Mathematicae (Proceedings). vol. 75, pp.
381–392. Elsevier (1972)

[13]
Deransart, P., Smaus, J.: Subject Reduction of Logic Programs as
Proof-Theoretic Property, vol. 2002 (2002),

[14]
Despeyroux, J.: A Higher-Order Specification of the pi-Calculus, Lecture
Notes in Computer Science, vol. 1872. Springer (2000).

[15]
Dybjer, P.: Inductive Families. Formal Asp. Comput.  6(4),  440–465
(1994). 10.1007/BF01211308

[16]
Gay, S.J.: A Framework for the Formalisation of Pi Calculus Type Systems in
Isabelle/HOL. In: Theorem Proving in Higher Order Logics, TPHOLs. Lecture
Notes in Computer Science, vol. 2152, pp. 217–232. Springer (2001).

[17]
Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session
types. J. Funct. Program.  20(1),  19–50 (2010).

[18]
Georges, A.L., Murawska, A., Otis, S., Pientka, B.: LINCX: A Linear Logical
Framework with First-Class Contexts. In: European Symposium on Programming,
ESOP, Lecture Notes in Computer Science, vol. 10201, pp. 530–555. Springer
(2017). 10.1007/978-3-662-54434-1_20

[19]
Goto, M.A., Jagadeesan, R., Jeffrey, A., Pitcher, C., Riely, J.: An extensible
approach to session polymorphism. Math. Struct. Comput. Sci.
26(3),  465–509 (2016). 10.1017/S0960129514000231

[20]
Honsell, F., Miculan, M., Scagnetto, I.: pi-calculus in (Co)inductive-type
theory. Theor. Comput. Sci.  253(2),  239–285 (2001).

[21]
Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L.,
Dreyer, D.: Iris: Monoids and invariants as an orthogonal basis for
concurrent reasoning. In: Rajamani, S.K., Walker, D. (eds.) Symposium on
Principles of Programming Languages, POPL 2015. pp. 637–650. ACM (2015).

[22]
Kobayashi, N.: Type Systems for Concurrent Programs (2007),
<http://www.kb.ecei.tohoku.ac.jp/ koba/papers/tutorial-type-extended.pdf>

[23]
Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the Pi-Calculus. In:
Symposium on Principles of Programming Languages, POPL. pp. 358–371. ACM
Press (1996). 10.1145/237721.237804

[24]
Mackie, I.: Lilac: A Functional Programming Language Based on Linear Logic.
J. Funct. Program.  4(4),  395–433 (1994).

[25]
Matsakis, N.D., II, F.S.K.: The rust language. In: High integrity language
technology, HILT. pp. 103–104. ACM (2014). 10.1145/2663171.2663188

[26]
McBride, C.: I Got Plenty o' Nuttin'. In: A List of Successes That Can Change
the World, Lecture Notes in Computer Science, vol. 9600, pp. 207–233.
Springer (2016). 10.1007/978-3-319-30936-1_12

[27]
Milner, R.: Communicating and mobile systems - the Pi-calculus. Cambridge
University Press (1999)

[28]
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, Parts I
and II. Inf. Comput.  100(1) (1992).

[29]
Orchard, D., Liepelt, V., III, H.E.: Quantitative program reasoning with
graded modal types. Proc. ACM Program. Lang.  3(ICFP),
110:1–110:30 (2019). 10.1145/3341714

[30]
Orchard, D.A., Yoshida, N.: Using session types as an effect system. In: Gay,
S., Alglave, J. (eds.) Programming Language Approaches to Concurrency- and
Communication-cEntric Software, PLACES 2015. EPTCS, vol. 203, pp. 1–13
(2015). 10.4204/EPTCS.203.1

[31]
Rouvoet, A., Poulsen, C.B., Krebbers, R., Visser, E.: Intrinsically-typed
definitional interpreters for linear, session-typed languages. In: Certified
Programs and Proofs, CPP. pp. 284–298. ACM (2020).

[32]
Sangiorgi, D., Walker, D.: The Pi-Calculus - a theory of mobile processes.
Cambridge University Press (2001)

[33]
Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A Linear Decomposition of
Multiparty Sessions for Safe Distributed Programming. In: European
Conference on Object-Oriented Programming, ECOOP. LIPIcs, vol. 74, pp.
24:1–24:31. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017).

[34]
Thiemann, P.: Intrinsically-Typed Mechanized Semantics for Session Types pp.
19:1–19:15 (2019). 10.1145/3354166.3354184

[35]
Turon, A.J., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical
relations for fine-grained concurrency. In: Giacobazzi, R., Cousot, R. (eds.)
Symposium on Principles of Programming Languages, POPL '13. pp. 343–356.
ACM (2013). 10.1145/2429069.2429111

[36]
Wadler, P.: Linear Types can Change the World! In: Programming concepts and
methods. p. 561. North-Holland (1990)

[37]
Zalakain, U., Dardha, O.: Typing the Linear $\pi$-Calculus –
Formalisation in Agda  (2021),