Programs are rarely implemented in a single language, and thus questions of type soundness should address not only the semantics of a single language, but how it interacts with others. Even between type-safe languages, disparate features can frustrate interoperability, as invariants from one language can easily be violated in the other. In their seminal 2007 paper, Matthews and Findler proposed a multi-language construction that augments the interoperating languages with a pair of \emph{boundaries} that allow code from one language to be embedded in the other. While this technique has been widely applied, their syntactic source-level interoperability doesn’t reflect practical implementations, where the behavior of interaction is only defined after compilation to a common target, and any safety must be ensured by target invariants or inserted target-level ``glue code.''

In this paper, we present a novel framework for the design and verification of sound language interoperability that follows an interoperation-after-compilation strategy. Language designers specify what data can be converted between types of the two languages via a convertibility relation $\tau_A \sim \tau_B$ (``$\tau_A$ is convertible to $\tau_B$'') and specify target-level glue code implementing the conversions. Then, by giving a semantic model of source-language types as sets of target-language terms, we can establish not only the meaning of our source types, but also \emph{soundness of conversions}: i.e., whenever $\tau_A \sim \tau_B$, the corresponding pair of conversions (glue code) convert target terms that behave like $\tau_A$ to target terms that behave like $\tau_B$, and vice versa. With this, we can prove semantic type soundness for the entire system. We illustrate our framework via a series of case studies that demonstrate how our semantic interoperation-after-compilation approach allows us both to account for complex differences in language semantics and make efficiency trade-offs based on particularities of compilers or targets.