The paper Operational Semantics for Multi-Language Programs
by Jacob Matthews and Robert Bruce Findler presents two approaches for defining the semantics of programs written in two programming languages, taking particular care of data defined in one language and used in the other. The lump embedding allows values created in one language to appear in running code of another, but these are can only be passed around, not operated on (or perhaps operated on by only a small interface).
The natural embedding allows values in one language to be used in the other by performing a so-called cross-language cast, which converts values from one language to the other.
The paper JNI Light: An Operational Model for the Core JNI by Gang Tan presents a formal semantics of how existing JNI works. In contrast to the previous paper, this is formalises many of the low level details of what's going on, rather than trying to explore the issues from a foundational perspective.
Work on type-checking foreign function calls, such as Checking Type Safety of Foreign Function Calls by Michael Furr and Jeffrey Foster, provide also a formal framework in which to phrase the type system and prove its soundness.
Looking at the references in these papers and finding where they are cited using google
scholar will help you discover a more thorough picture of what has been done in the area.