MixML linking and definedness

For ${\mathsf{Mix}}_0$, $\mathrm{\Omega }$ maps slots to core types, $D$ is the defined subset, and signatures contain imports $p^{-}:A$ and exports $p^{+}:A$. The operation ${\ell }^{-1}$ selects the entries below label $\ell$ and removes that prefix. The complete primitive transition rules are

$\mathrm{\Omega }(p)=A$

$\mathrm{\Omega };D⊢\mathsf{imp}(p:A):\{p^{-}:A\}\Rightarrow D$

$\mathrm{\Omega }(p)=A$$\mathrm{\Omega };D{⊢}_{\mathsf{core}}e:A$$p\notin D$$\mathsf{wr}(e)=\{p\}$

$\mathrm{\Omega };D⊢\mathsf{def}(p=e:A):\{p^{+}:A\}\Rightarrow D\cup \{p\}$

$\mathrm{\Omega };D⊢M:{\mathrm{\Sigma }}_1\Rightarrow D_1$$\mathrm{\Omega };D_1⊢N:{\mathrm{\Sigma }}_2\Rightarrow D_2$$\mathsf{merge}({\mathrm{\Sigma }}_1,{\mathrm{\Sigma }}_2)=\mathrm{\Sigma }$

$\mathrm{\Omega };D⊢M\mathsf{with}N:\mathrm{\Sigma }\Rightarrow D_2$

${\ell }^{-1}\mathrm{\Omega };{\ell }^{-1}D⊢M:\mathrm{\Sigma }\Rightarrow D_0$

$\mathrm{\Omega };D⊢\{\ell =M\}:\ell \cdot \mathrm{\Sigma }\Rightarrow (D\setminus \ell \cdot ({\ell }^{-1}D))\cup \ell \cdot D_0$

$\mathrm{\Omega };D⊢M:\mathrm{\Sigma }\Rightarrow D^{\prime }$$Q\subseteq \mathrm{dom}(\mathrm{\Sigma })$$\mathrm{\Sigma }{|}_Q={\mathrm{\Sigma }}_0$

$\mathrm{\Omega };D⊢{\mathsf{seal}}_{{\mathrm{\Sigma }}_0}(M):{\mathrm{\Sigma }}_0\Rightarrow D^{\prime }$

$\mathrm{\Omega };D⊢M:\mathrm{\Sigma }\Rightarrow D^{\prime }$$\mathrm{\forall }p\in \mathrm{dom}(\mathrm{\Sigma }).\mathrm{\exists }A.\mathrm{\Sigma }(p)=p^{+}:A$

$\mathrm{\Omega };D⊢\mathsf{complete}(M):\mathrm{\Sigma }\Rightarrow D^{\prime }$

The ordered slot checker extracts traces by

${\mathrm{\Xi }}^U{⊢}_{\mathsf{v}}v:A$

$\mathrm{\Xi }⊢\mathsf{return}v:A\Rightarrow \mathrm{\Xi }▹ϵ$

$\mathrm{\Xi }={\mathrm{\Xi }}_0,x:A^U$

$\mathrm{\Xi }⊢\mathsf{get}x:A\Rightarrow \mathrm{\Xi }▹\mathsf{get}x$

$\mathrm{\Xi }={\mathrm{\Xi }}_0,x:A^L$${\mathrm{\Xi }}_0^U{⊢}_{\mathsf{v}}v:A$

$\mathrm{\Xi }⊢\mathsf{set}xv:\mathbf{1}\Rightarrow {\mathrm{\Xi }}_0,x:A^U▹\mathsf{set}x$

$\mathrm{\Xi }⊢c_1:\mathbf{1}\Rightarrow {\mathrm{\Xi }}_1▹t_1$${\mathrm{\Xi }}_1⊢c_2:B\Rightarrow {\mathrm{\Xi }}_2▹t_2$

$\mathrm{\Xi }⊢c_1;c_2:B\Rightarrow {\mathrm{\Xi }}_2▹t_1\cdot t_2$

$x\notin \mathrm{dom}(\mathrm{\Xi })\cup \mathrm{dom}({\mathrm{\Xi }}^{\prime })$$\mathrm{\Xi },x:A^L⊢c:B\Rightarrow {\mathrm{\Xi }}^{\prime },x:A^U▹t$

$\mathrm{\Xi }⊢{\mathsf{new}}_A(x.c):B\Rightarrow {\mathrm{\Xi }}^{\prime }▹\nu x.t$

The corresponding trace validator is

$\mathrm{\Xi }{⊢}_{\mathsf{tr}}ϵ\Rightarrow \mathrm{\Xi }$

$\mathrm{\Xi }={\mathrm{\Xi }}_0,x:A^U$

$\mathrm{\Xi }{⊢}_{\mathsf{tr}}\mathsf{get}x\Rightarrow \mathrm{\Xi }$

$\mathrm{\Xi }={\mathrm{\Xi }}_0,x:A^L$

$\mathrm{\Xi }{⊢}_{\mathsf{tr}}\mathsf{set}x\Rightarrow {\mathrm{\Xi }}_0,x:A^U$

$\mathrm{\Xi }{⊢}_{\mathsf{tr}}{t}_1\Rightarrow {\mathrm{\Xi }}_1$${\mathrm{\Xi }}_1{⊢}_{\mathsf{tr}}{t}_2\Rightarrow {\mathrm{\Xi }}_2$

$\mathrm{\Xi }{⊢}_{\mathsf{tr}}{t}_1\cdot t_2\Rightarrow {\mathrm{\Xi }}_2$

$x\notin \mathrm{dom}(\mathrm{\Xi })\cup \mathrm{dom}({\mathrm{\Xi }}^{\prime })$$\mathrm{\Xi },x:A^L{⊢}_{\mathsf{tr}}t\Rightarrow {\mathrm{\Xi }}^{\prime },x:A^U$

$\mathrm{\Xi }{⊢}_{\mathsf{tr}}\nu x.t\Rightarrow {\mathrm{\Xi }}^{\prime }$

This checker is stricter than LTG. Full LTG has stores $s::=ϵ\mid s,x:?\tau \mid s,x:=e:\tau$, the split $(?\tau {)}^L\ast (?\tau {)}^U=(?\tau {)}^L$, and the two dereference reductions

The imported MixML rules use semantic signatures $$\mathrm{\Sigma }::=[[=A]]\mid [[A{]]}^{\pm }\mid [[\mathrm{\Phi }{]]}^{\pm }\mid \{|\ell :\mathrm{\Sigma }|\},\mathrm{\Phi }::=\mathrm{\forall }\overline{\alpha }.\mathrm{\exists }\overline{\beta }.(L_{\mathsf{i}};L_{\mathsf{e}};\mathrm{\Sigma }).$$ Their deterministic link rule first computes both templates, then runs the static right-hand pass, bidirectional locator lookup, the two main checks, and the final semantic-signature merge, exactly as (15.2)–(15.5).