Fully Abstract Compilation

\[P_1 \sim^{S} P_2 \Leftrightarrow [|P_1|]\_{T}^{S} \sim^{T} [|P_2|]^{S}_{T}\]