We prove each part separately.

  1. (1)

Type environment
$\Gamma^{\infty}(D_{\mathcal{G}})=\Gamma_{\mathcal{V}(D_{\mathcal{G}})}$ is
constructed inductively in parallel to an automaton approximation, which means
there exists a linear order of environments
$\Gamma_{0},\Gamma_{1},\dots,\Gamma_{n}$ where $\Gamma_{0}=\emptyset$ and
$\Gamma_{n}=\Gamma_{\mathcal{V}(D_{\mathcal{G}})}$ and
$\Gamma_{i}=\Gamma_{i-1}\uplus\\{{f_{i}}::{\mathsf{fromCl}({\forall\overline{{y}}.\,U_{i}\Rightarrow
P_{i}\,(f_{i}\,\overline{{y}})})}\\}$, for all $1\leq i\leq n$, such that
there exists $(\forall\overline{{y}}.\,G_{i}\Rightarrow
P_{i}\,(f_{i}\,\overline{{y}}))\in D_{\mathcal{G}}$ and $V_{\Gamma_{i}}\vdash
G_{i}\triangleright^{*}U_{i}$.

By a straightforward induction with Lemma D.8, each $\Gamma_{i}$ is
${\mathcal{G}}$-coconsistent. Therefore, so is
$\Gamma^{\infty}(D_{\mathcal{G}})=\Gamma_{\mathcal{V}(D_{\mathcal{G}})}$.

  2. (2)

Suppose ${\uparrow_{\mathsf{a}}}(V),\overline{{y}}\vdash
G\triangleright^{*}U$. Clearly,
$V\mathrel{\leq_{\mathsf{a}}}{\uparrow_{\mathsf{a}}}(V)$. Starting from the
end of the rewrite, we inductively replace each application of (Step) with a
$T^{\prime}\in{\uparrow_{\mathsf{a}}}(V)$ by (Step) with a smaller $T\in V$,
which exists by Subtyping Lemma D.1. (We do not need to consider (Refl),
because $P\,x\in{\uparrow_{\mathsf{a}}}(V)$ if and only if $P\,x\in V$.)

Suppose ${\uparrow_{\mathsf{a}}}(V),\overline{{y}}\vdash G\triangleright
G^{\prime}\triangleright^{n}U$ where
${\uparrow_{\mathsf{a}}}(V),\overline{{y}}\vdash G\triangleright G^{\prime}$
is the only step to use an automaton clause from
${\uparrow_{\mathsf{a}}}(V)\backslash V$. Let
$T^{\prime}=(\forall\overline{{x}}.\,U_{0}^{\prime}\Rightarrow
P\,(f\,\overline{{x}}))\in{\uparrow_{\mathsf{a}}}(V)$ be the side condition,
so $G=P\,(f\,\overline{{s}})$ and
$G^{\prime}=U_{0}^{\prime}[\overline{{s}}/\overline{{x}}]$. Let
$T=(\forall\overline{{x}}.\,U_{0}\Rightarrow P\,(f\,\overline{{x}}))\in V$
such that $T\mathrel{\leq_{\mathsf{a}}}T^{\prime}$. This means
$U_{0}^{\prime}\mathrel{\leq_{\mathsf{a}}}U_{0}$.

By monotonicity of rewrite (Lemma D.5), there exists $U^{\prime}$ such that
$U\mathrel{\leq_{\mathsf{a}}}U^{\prime}$ and $V,\overline{{y}}\vdash
G\triangleright
U_{0}[\overline{{s}}/\overline{{x}}]\triangleright^{n}U^{\prime}$.

  3. (3)

Suppose $V_{1}\mathrel{\leq_{\mathsf{a}}}V_{2}$ over variables
$\overline{{y}}$. By definition, for all $y\in\overline{{y}}$,
$\mathsf{fromCl}({{V_{1}}_{|{y}}})\leq\mathsf{fromCl}({{V_{2}}_{|{y}}})$. By
Subtyping Lemma D.1, for every $\tau_{2}\in\mathsf{fromCl}({{V_{2}}_{|{y}}})$,
there exists $\tau_{1}\in\mathsf{fromCl}({{V_{1}}_{|{y}}})$ such that
$\tau_{1}\leq\tau_{2}$, which is
$\mathsf{toCl}({\tau_{1}})({y})\mathrel{\leq_{\mathsf{a}}}\mathsf{toCl}({\tau_{2}})({y})$
in the clause setting.

Clearly,
$\mathsf{toCl}({\tau_{2}})({y})\in{\uparrow_{\mathsf{a}}}(\mathsf{toCl}({\tau_{1}})({y}))$.
It follows from
$\mathsf{toCl}({\tau_{1}})({y})\in\mathsf{fromCl}({{V_{1}}_{|{y}}})$ and
$\mathsf{toCl}({\tau_{2}})({y})\in\mathsf{fromCl}({{V_{2}}_{|{y}}})$ that
$V_{2}\subseteq{\uparrow_{\mathsf{a}}}(V_{1})$, as required.

  4. (4)

We use induction on the size of $\Gamma$. If $\Gamma$ is empty, then
$V_{\Gamma}=\emptyset\subseteq\mathcal{V}(D_{\mathcal{G}})$, so suppose
$\Gamma$ is ${\mathcal{G}}$-coconsistent and non-empty.

As per Lemma D.8, let $(\forall\overline{{y}}.\,U\Rightarrow
P\,(f\,\overline{{y}}))\in V_{\Gamma}$ and
$(\forall\overline{{y}}.\,G\Rightarrow P\,(f\,\overline{{y}}))\in
D_{\mathcal{G}}$ such that:

$\Gamma\backslash\\{{f}::{\tau}\\}\text{ is }{\mathcal{G}}\text{-coconsistent
and }\exists
U^{\prime}.\,V_{\Gamma\backslash\\{{f}::{\tau}\\}},\overline{{y}}\vdash
G\triangleright^{*}U^{\prime}\land U\mathrel{\leq_{\mathsf{a}}}U^{\prime}$

where $\tau=\mathsf{fromCl}({\forall\overline{{y}}.\,U\Rightarrow
P\,(f\,\overline{{y}})})$.

By the IH,
$\mathcal{V}(D_{\mathcal{G}})\mathrel{\leq_{\mathsf{a}}}V_{\Gamma\backslash\\{{f}::{\tau}\\}}$.
Now, 3 gives us
$V_{\Gamma\backslash\\{{f}::{\tau}\\}}\subseteq{\uparrow_{\mathsf{a}}}(\mathcal{V}(D_{\mathcal{G}}))$.
Thus, rewrite $V_{\Gamma\backslash\\{{f}::{\tau}\\}},\overline{{y}}\vdash
G\triangleright^{*}U^{\prime}$ gives us
${\uparrow_{\mathsf{a}}}(\mathcal{V}(D_{\mathcal{G}})),\overline{{y}}\vdash
G\triangleright^{*}U^{\prime}$. By 2,
$\mathcal{V}(D_{\mathcal{G}}),\overline{{y}}\vdash
G\triangleright^{*}U^{\prime\prime}$ for some $U^{\prime\prime}$ such that
$U^{\prime}\mathrel{\leq_{\mathsf{a}}}U^{\prime\prime}$. Transitivity yields
$U\mathrel{\leq_{\mathsf{a}}}U^{\prime\prime}$.

Since
$V_{\Gamma}=V_{\Gamma\backslash\\{{f}::{\tau}\\}}\land\mathsf{toCl}({\tau})({f})$,
it remains to show that
$\mathcal{V}(D_{\mathcal{G}})\mathrel{\leq_{\mathsf{a}}}\mathsf{toCl}({\tau})({f})$,
which is
$\mathcal{V}(D_{\mathcal{G}})\mathrel{\leq_{\mathsf{a}}}\forall\overline{{y}}.\,U\Rightarrow
P\,(f\,\overline{{y}})$. Now, $(\forall\overline{{y}}.\,G\Rightarrow
P\,(f\,\overline{{y}}))\in D_{\mathcal{G}}$ and
$\mathcal{V}(D_{\mathcal{G}}),\overline{{y}}\vdash
G\triangleright^{*}U^{\prime\prime}$ satisfy the side conditions of the
rewrite algorithm for including
$(\forall\overline{{y}}.\,U^{\prime\prime}\Rightarrow P\,(f\,\overline{{y}}))$
in $\mathcal{V}(D_{\mathcal{G}})$.

Finally, $U\mathrel{\leq_{\mathsf{a}}}U^{\prime\prime}$ implies
$(\forall\overline{{y}}.\,U^{\prime\prime}\Rightarrow
P\,(f\,\overline{{y}}))\mathrel{\leq_{\mathsf{a}}}(\forall\overline{{y}}.\,U\Rightarrow
P\,(f\,\overline{{y}}))$, so
$(\forall\overline{{y}}.\,U^{\prime\prime}\Rightarrow
P\,(f\,\overline{{y}}))\in\mathcal{V}(D_{\mathcal{G}})$ gives us
$\mathcal{V}(D_{\mathcal{G}})\mathrel{\leq_{\mathsf{a}}}(\forall\overline{{y}}.\,U\Rightarrow
P\,(f\,\overline{{y}}))$, which concludes the proof.

  5. (5)

Suppose $\Gamma\vdash{t}::{\tau}$ and $\Gamma$ is
${\mathcal{G}}$-coconsistent. By 4,
$\mathcal{V}(D_{\mathcal{G}})\mathrel{\leq_{\mathsf{a}}}V_{\Gamma}$, which
means $\Gamma_{\mathcal{V}(D_{\mathcal{G}})}\leq\Gamma_{V_{\Gamma}}=\Gamma$.
By Lemma 3.2.3 from Ramsay (2014), there exists $\tau^{\prime}$ such that
$\Gamma_{\mathcal{V}(D_{\mathcal{G}})}\vdash{t}::{\tau^{\prime}}$ and
$\tau^{\prime}\leq\tau$.

∎

See 5.9

###### Proof.

We prove the following:

$\exists{\mathcal{G}}\text{-coconsistent
}\Gamma.\,\Gamma\vdash{t}::{\tau}\text{ if, and only if,
}\mathcal{V}(D_{\mathcal{G}})\vdash\mathsf{toCl}({\tau})({t})\triangleright^{*}\mathsf{true}$

For direction $\Leftarrow$, suppose
$\mathcal{V}(D_{\mathcal{G}})\vdash\mathsf{toCl}({\tau})({t})\triangleright^{*}\mathsf{true}$.
Since
$\Gamma^{\infty}(D_{\mathcal{G}})=\Gamma_{\mathcal{V}(D_{\mathcal{G}})}$,
Proposition 5.6 gives us $\Gamma^{\infty}(D_{\mathcal{G}})\vdash{t}::{\tau}$.
We know from 1 that $\Gamma^{\infty}(D_{\mathcal{G}})$ is
${\mathcal{G}}$-coconsistent, which proves the claim.

For direction $\Rightarrow$, suppose there exists a
${\mathcal{G}}$-coconsistent $\Gamma$ such that $\Gamma\vdash{t}::{\tau}$. By
5, there exists $\tau^{\prime}$ such that
$\Gamma_{\mathcal{V}(D_{\mathcal{G}})}\vdash{t}::{\tau^{\prime}}$ and
$\tau^{\prime}\leq\tau$. Proposition 5.6 gives us
$\mathcal{V}(D_{\mathcal{G}})\vdash\mathsf{toCl}({\tau^{\prime}})({t})\triangleright^{*}\mathsf{true}$.
Finally, Lemma D.5 gives us
$\mathcal{V}(D_{\mathcal{G}})\vdash\mathsf{toCl}({\tau})({t})\triangleright^{*}\mathsf{true}$.
∎

##  Appendix E Supporting Material for Section 6

Figure 11 lists the definite clauses that capture the behaviour of sockets in
our automated verifier for socket-manipulating Haskell programs. These
program-independent clauses are included in the MSL($\omega$) definite clause
that captures the socket usage in the input Haskell program.

$\displaystyle\textsf{Untracked}\ (\mathtt{socket}\ k)$
$\displaystyle\Leftarrow\textsf{Ready}\ (k\ \underline{s})$
$\displaystyle\textsf{Untracked}\ (\mathtt{socket}\ k)$
$\displaystyle\Leftarrow\textsf{Untracked}\ (k\ \underline{u})$
$\displaystyle\textsf{Untracked}\ (\mathtt{bind}\ k\ \underline{u})$
$\displaystyle\Leftarrow\textsf{Untracked}\ k$
$\displaystyle\textsf{Untracked}\ (\mathtt{connect}\ k\ \underline{u})$
$\displaystyle\Leftarrow\textsf{Untracked}\ k$
$\displaystyle\textsf{Untracked}\ (\mathtt{listen}\ k\ \underline{u})$
$\displaystyle\Leftarrow\textsf{Untracked}\ k$
$\displaystyle\textsf{Untracked}\ (\mathtt{accept}\ k\ \underline{u})$
$\displaystyle\Leftarrow\textsf{Open}\ (k\ \underline{s})$
$\displaystyle\textsf{Untracked}\ (\mathtt{accept}\ k\ \underline{u})$
$\displaystyle\Leftarrow\textsf{Untracked}\ (k\ \underline{u})$
$\displaystyle\textsf{Untracked}\ (\mathtt{close}\ k\ \underline{u})$
$\displaystyle\Leftarrow\textsf{Untracked}\ k$
$\displaystyle\textsf{Untracked}\ (\mathtt{send}\ k\ \underline{u})$
$\displaystyle\Leftarrow\textsf{Untracked}\ k$
$\displaystyle\textsf{Untracked}\ (\mathtt{receive}\ k\ \underline{u})$
$\displaystyle\Leftarrow\textsf{Untracked}\ k$ $\displaystyle\textsf{Ready}\
(\mathtt{bind}\ k\ \underline{s})$ $\displaystyle\Leftarrow\textsf{Bound}\
(k)$ $\displaystyle\textsf{Ready}\ (\mathtt{connect}\ k\ \underline{s})$
$\displaystyle\Leftarrow\textsf{Open}\ (k)$ $\displaystyle\textsf{Ready}\
(\mathtt{listen}\ k\ \underline{s})$ $\displaystyle\Leftarrow$
$\displaystyle\textsf{Ready}\ (\mathtt{accept}\ k\ \underline{s})$
$\displaystyle\Leftarrow$ $\displaystyle\textsf{Ready}\ (\mathtt{close}\ k\
\underline{s})$ $\displaystyle\Leftarrow$ $\displaystyle\textsf{Ready}\
(\mathtt{send}\ k\ \underline{s})$ $\displaystyle\Leftarrow$
$\displaystyle\textsf{Ready}\ (\mathtt{receive}\ k\ \underline{s})$
$\displaystyle\Leftarrow$ $\displaystyle\textsf{Bound}\ (\mathtt{bind}\ k\
\underline{s})$ $\displaystyle\Leftarrow$ $\displaystyle\textsf{Bound}\
(\mathtt{connect}\ k\ \underline{s})$ $\displaystyle\Leftarrow$
$\displaystyle\textsf{Bound}\ (\mathtt{listen}\ k\ \underline{s})$
$\displaystyle\Leftarrow\textsf{Listening}\ (k)$ $\displaystyle\textsf{Bound}\
(\mathtt{accept}\ k\ \underline{s})$ $\displaystyle\Leftarrow$
$\displaystyle\textsf{Bound}\ (\mathtt{close}\ k\ \underline{s})$
$\displaystyle\Leftarrow$ $\displaystyle\textsf{Bound}\ (\mathtt{send}\ k\
\underline{s})$ $\displaystyle\Leftarrow$ $\displaystyle\textsf{Bound}\
(\mathtt{receive}\ k\ \underline{s})$ $\displaystyle\Leftarrow$
$\displaystyle\textsf{Listening}\ (\mathtt{bind}\ k\ \underline{s})$
$\displaystyle\Leftarrow$ $\displaystyle\textsf{Listening}\ (\mathtt{connect}\
k\ \underline{s})$ $\displaystyle\Leftarrow$ $\displaystyle\textsf{Listening}\
(\mathtt{listen}\ k\ \underline{s})$ $\displaystyle\Leftarrow$
$\displaystyle\textsf{Listening}\ (\mathtt{accept}\ k\ \underline{s})$
$\displaystyle\Leftarrow\textsf{Listening}\ (k\ \underline{u})$
$\displaystyle\textsf{Listening}\ (\mathtt{close}\ k\ \underline{s})$
$\displaystyle\Leftarrow$ $\displaystyle\textsf{Listening}\ (\mathtt{send}\ k\
\underline{s})$ $\displaystyle\Leftarrow$ $\displaystyle\textsf{Listening}\
(\mathtt{receive}\ k\ \underline{s})$ $\displaystyle\Leftarrow$

$\displaystyle\textsf{Open}\ (\mathtt{bind}\ k\ \underline{s})$
$\displaystyle\Leftarrow$ $\displaystyle\textsf{Open}\ (\mathtt{connect}\ k\
\underline{s})$ $\displaystyle\Leftarrow$ $\displaystyle\textsf{Open}\
(\mathtt{listen}\ k\ \underline{s})$ $\displaystyle\Leftarrow$
$\displaystyle\textsf{Open}\ (\mathtt{accept}\ k\ \underline{s})$
$\displaystyle\Leftarrow$ $\displaystyle\textsf{Open}\ (\mathtt{close}\ k\
\underline{s})$ $\displaystyle\Leftarrow\textsf{Close}\ (k)$
$\displaystyle\textsf{Open}\ (\mathtt{send}\ k\ \underline{s})$
$\displaystyle\Leftarrow\textsf{Open}\ (k)$ $\displaystyle\textsf{Open}\
(\mathtt{receive}\ k\ \underline{s})$ $\displaystyle\Leftarrow\textsf{Open}\
(k)$ $\displaystyle\textsf{Close}\ (\mathtt{bind}\ k\ \underline{s})$
$\displaystyle\Leftarrow$ $\displaystyle\textsf{Close}\ (\mathtt{connect}\ k\
\underline{s})$ $\displaystyle\Leftarrow$ $\displaystyle\textsf{Close}\
(\mathtt{listen}\ k\ \underline{s})$ $\displaystyle\Leftarrow$
$\displaystyle\textsf{Close}\ (\mathtt{accept}\ k\ \underline{s})$
$\displaystyle\Leftarrow$ $\displaystyle\textsf{Close}\ (\mathtt{close}\ k\
\underline{s})$ $\displaystyle\Leftarrow$ $\displaystyle\textsf{Close}\
(\mathtt{send}\ k\ \underline{s})$ $\displaystyle\Leftarrow$
$\displaystyle\textsf{Close}\ (\mathtt{receive}\ k\ \underline{s})$
$\displaystyle\Leftarrow$ $\displaystyle\forall\ q\in
Q\setminus\\{\textsf{Untracked}\\}.\hskip 40.0pt$ $\displaystyle q\
(\mathtt{socket}\ k)$ $\displaystyle\Leftarrow q\ (k\ \underline{u})$
$\displaystyle q\ (\mathtt{bind}\ k\ \underline{u})$ $\displaystyle\Leftarrow
q\ (k)$ $\displaystyle q\ (\mathtt{connect}\ k\ \underline{u})$
$\displaystyle\Leftarrow q\ (k)$ $\displaystyle q\ (\mathtt{listen}\ k\
\underline{u})$ $\displaystyle\Leftarrow q\ (k)$ $\displaystyle q\
(\mathtt{accept}\ k\ \underline{u})$ $\displaystyle\Leftarrow q\ (k)$
$\displaystyle q\ (\mathtt{close}\ k\ \underline{u})$ $\displaystyle\Leftarrow
q\ (k)$ $\displaystyle q\ (\mathtt{send}\ k\ \underline{u})$
$\displaystyle\Leftarrow q\ (k)$ $\displaystyle q\ (\mathtt{receive}\ k\
\underline{u})$ $\displaystyle\Leftarrow q\ (k)$

Figure 11. Clauses defining the behaviour of socket programs