In practice, FFIs are implemented by translation to a target language and by conversions at the level of the target. We wish to establish type soundness in such a setting, where there are two languages making foreign calls to one another. In particular, we want a notion of \emph{convertibility}, that a type $\tau_A$ from language $A$ is convertible to a type $\tau_B$ from language $B$, which we will write $\tau_A \sim \tau_B$, such that conversions between these types maintain type soundness (dynamically or statically) of the overall system.

In this paper, we leverage the idea that sound FFIs are a generalization of sound gradual typing, except unlike gradual typing, FFIs mediate between languages \emph{without} a common underlying term language. We start with two languages and define type soundness in a manner inspired by the practical implementation strategy: that the languages will be translated to a common target. We do this using a realizability model, that is, by setting up a logical relation indexed by source types but inhabited by target terms that behave as dictated by the source types. The conversions $\tau_A \sim \tau_B$ that \emph{should} be allowed, are the ones implemented by target-level translations that convert terms that semantically behave like $\tau_A$ to terms that semantically behave like $\tau_B$ (and vice versa). This means that the converted term must either produce a runtime cast failure or produce some term or value that behaves as $\tau_B$. With the notion of $\tau_A \sim \tau_B$ in hand, we can type check a foreign function call, and based on the semantics of
$\tau_A \sim \tau_B$, we can prove that typing the foreign function call is sound.