ICFP 2006

Paper: submitted. This is the multi-language semantics paper I've been working on forever; the one that was going to be an ICFP '05 paper, then a POPL '06 paper, and then an ESOP paper, but we never ended up submitting to any of those places because it wasn't ever finished. Now it's finally finished, so there's nothing left to do but hope.

It's called "The Meaning of Multi-Language Programs" and it's by me and Robby Findler. Here's the abstract:

Interoperability is big business, a fact to which .NET, the JVM, and COM can attest. Language designers are well aware of this, and they are designing programming languages that reflect it --- SML#, Mondrian, and Scala all treat interoperability as a central design feature, just to name a few. Still, current multi-language research tends not to focus on these languages' semantics, but only on how to implement them efficiently. In this paper, we attempt to rectify that by giving a technique for modeling a multi-language system as a composition of the models of its constituent languages. Our technique abstracts away the low-level details of interoperability like garbage collection and representation coherence, and lets us focus on semantic properties like type-safety and termination behavior.

We demonstrate the technique with a series of strategies for embedding a Scheme-like language into an ML-like language. We will start by connecting very simple languages with a very simple strategy, and work our way up to languages with sophisticated features like effects and that interact in sophisticated ways. Along the way, we prove type-soundness for each system we present. Our technique allows these proofs to be straightforward generalizations of standard type-soundness proofs for single languages.

Beyond giving simple expressive models, our studies have uncovered several interesting facts about interoperability. For example, higher-order function contracts naturally emerge as the glue to ensure that interoperating languages respect each other's type systems. Our models also predict that the embedding strategy where foreign values are opaque is as expressive as the embedding strategy where foreign values are translated to corresponding values in the other language, and we were able to experimentally verify this behavior using PLT Scheme's foreign function interface.

Once I'm ready to put the full paper online I'll post a link.