Interoperability pervades nearly all mainstream language implementations, as
most systems leverage subcomponents written in different languages. And yet,
such linking can expose a language to foreign behaviors that are internally
inexpressible, which poses a serious threat to safety invariants and programmer
reasoning. To preserve such invariants, a language may try to add features to limit
the reliance on external libraries, but endless extensions can obscure the core
abstractions the language was designed to provide.

In this paper, we outline an approach that
encapsulates foreign code in a sound way—i.e., without disturbing the
invariants promised by types of the core language. First, one introduces novel
\emph{linking types} that characterize the behaviors of
foreign libraries that are inexpressible in the core language.
To reason about the soundness of linking,
one constructs a \emph{realizability model} that captures the meaning
of both core types and linking types as sets of target-language terms.
Using this model, one can formally prove when foreign behavior is \emph{encapsulated};
that is, unobservable to core code.
We show one way to discharge such proofs automatically by augmenting the compiler to insert verified \emph{encapsulation wrappers}
around components that use foreign libraries.

Inspired by existing approaches to FFIs, we develop a pair of case studies that
extend a pure, functional language: one extension for state, and another for
exceptions. The first allows us to implement mutable references via a library,
whereas the second allows us to implement $\mathtt{try}$ and $\mathtt{catch}$ as
library functions. Both extensions and the overall system are proven sound using logical relations that use realizability techniques.