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 & Yoshida are attempting to do (Theorems 1- 5), although they don't quite achieve it.