Semantic Apparatus – Semantic Soundness for Language Interoperability

Cited by Lee Sonogan

Conversational Interoperability - Oliver Meredith Cox


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 [43] proposed a a multi-language construction that augments the interoperating languages with a pair of boundaries that allow code from one language to be embedded in the other. While this technique has been widely applied, their 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-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 𝜏𝐴 ∼ 𝜏𝐡 (β€œπœπ΄ is convertible to 𝜏𝐡 ”) 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 soundness of conversions: i.e., whenever 𝜏𝐴 ∼ 𝜏𝐡 , the corresponding pair of conversions (glue code) convert target terms that behave like 𝜏𝐴 to target terms that behave like 𝜏𝐡 , 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 and show how the approach helps designers better take advantage of efficient enforcement mechanisms and opportunities for sound sharing that may not be obvious in a setting divorced from implementations.

Publication: Northeastern University, USA (Peer-Reviewed Journal)

Pub Date: 2021 Doi:

Keywords: language interoperability, type soundness, semantics, logical relations (Plenty more sections and references in this research article)

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.