used to define types that organise into a denotational semantics for MLL (a $\ast$-autonomous category), and prove soundness and completeness of the model w.r.t. MLL+MIX, an extension of MLL with the so-called MIX rule (Theorems \[thm:soundness\] & \[thm:completeness\]).

Stellar Resolution {#sec:stellar}
==================

First-order Terms and Unification {#subsec:unifcation}
---------------------------------

Stellar resolution is based on the theory of unification. We here recall basic definitions and refer the reader to the article of *Lassez et al.* [@lassez1988unification] for more details.

\[def:signature\] A signature $\mathbb{S} = (\mathcal{V}, \mathcal{F}, \mathtt{ar})$ consists of an infinite countable set $\mathcal{V}$ of variables, a countable set $\mathcal{F}$ of function symbols whose arities are given by $\mathtt{ar} : \mathcal{F} \rightarrow \nat$.

\[def:term\] Let $\mathbb{S} = (\mathcal{V}, \mathcal{F}, \mathtt{ar})$ be a signature. The set of terms $\mathcal{T}_\mathbb{S}$ is inductively defined by the grammar $t, u ::= x \mid f(t_1, ..., t_n)$ with $x \in \mathcal{V}, f \in \mathcal{F}, \mathtt{ar}(f) = n$.

We now fix a signature $\mathbb{S} = (\mathcal{V}, \mathcal{F}, \mathtt{ar})$ until the end of this section.

\[def:subst\]\[def:rename\] A substitution is a function $\theta: \mathcal{V} \rightarrow \mathcal{T}_\mathbb{S}$ extended from variables to terms by $\theta(f(u_1, ..., u_k)) = f(\theta u_1, ..., \theta u_k)$.

A *renaming* is a substitution $\alpha$ such that $\alpha(x)\in\mathcal{V}$ 