How to prove relations between "classes" of types?
One approach to such questions is via encodings.  

Say you have a language $L_1$ and a language $L_2$ and you want to show that they are somehow "the same", you can do this by finding an encoding

$$
   \newcommand{\SEMBTYPE}[1]{\ulcorner #1 \urcorner}
   \newcommand{\SEMB}[1]{\lbrack\!\lbrack #1 \rbrack\!\rbrack}
    \SEMB{\cdot} : L_1 \rightarrow L_2
$$

and then show that for all $L_1$ programs $M, N$ the following holds:

$$
   M \cong_1 N
   \qquad \text{iff} \qquad
   \SEMB{M_1} \cong_2 \SEMB{M_2}
$$

Here $\cong_i$ is a chosen notion of program equivalence for $L_i$. In order to do this for typed languages, one typically also maps $L_1$-types to $L_2$ by way of a function $\SEMBTYPE{\cdot}$ which is extended to typing environments, such that
something like the following holds:

$$
   \Gamma \vdash_1 M : \alpha
   \qquad \text{implies} \qquad
   \SEMBTYPE{\Gamma} \vdash_2 \SEMB{M} : \SEMBTYPE{\alpha}
$$
Here $\vdash_i$ is the typing judgement for $L_i$. 
The whole approach is called full abstraction.

In order to avoid the "curse of Church-Turing universality", one typically imposes conditions on $\SEMB{\cdot}$, e.g. that it's compositional, or closed under injective renaming. The more conditions $\SEMB{\cdot}$ meets, the stronger the full abstraction result.

This is also Orchard &amp; Yoshida are attempting to do (Theorems 1- 5), although they don't quite achieve it.