Operational Semantics for Multi-Language Programs

Jacob Matthews, Robert Bruce Findler

Inter-language interoperability is big business, as the success of Microsoft's .NET and COM and Sun's JVM show. Programming language designers are designing programming languages that reflect that fact — SML#, Mondrian, and Scala, to name just a few examples, all treat interoperability with other languages as a central design feature. Still, current multi-language research tends not to focus on the semantics of interoperation features, but only on how to implement them efficiently. In this paper, we take first steps toward higher-level models of interoperating systems. 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 observable equivalence.

Beyond giving simple expressive models that are natural compositions of single-language models, our studies have uncovered several interesting facts about interoperability. For example, higher-order contracts naturally emerge as the glue to ensure that interoperating languages respect each other's type systems. While we present our results in an abstract setting, they shed light on real multi-language systems and tools such as the JNI, SWIG, and Haskell's stable pointers.

Thank you for your interest in our work! Here you can download a number of resources related to our paper.

  • The systems from the paper — available as a tarball: paper-systems.tar.gz or browsable online. These systems are implemented as programs with test suites written in SchemeUnit, the unit-testing suite written by the Schematics project. Each reduction system (defined in a file called section-number-description.ss) corresponds to a particular figure from the paper; the other files define tests and support code. To try out example terms in any language:
    1. Download paper-systems.tar.gz and unpack it anywhere you'd like.
    2. Install the latest version of DrScheme (you need at least version 350)
    3. Start DrScheme and set its language level to (module ...) in the Language > Choose Language ... menu.
    4. Open the file that corresponds to the system you want in DrScheme and click the green "Run" button at the top of the screen. This will take a while the first time you do it, because DrScheme is automatically downloading, compiling and installing PLT Redex and SchemeUnit.
    5. The DrScheme window should be split into a definitions pane at the top and an interactions pane at the bottom. In the interactions pane, the function gui has been loaded, and you can use it to execute programs. To execute a program, type:
      (gui (quote [the program to execute]))
      The system will respond by popping up a GUI window that illustrates the reduction sequence for the given term. Unfortunately the syntax that PLT Redex recognizes is slightly different from the syntax used in the paper. You can see many example terms in the test suites that come in the distribution file, but these guidelines will help:
      Paper syntaxPLT Redex syntax
      (λ x: ι. (+ x 1)) (lambda (x : num) (+ x 1))
      MSι → ι → ι (λ x. λ y. y) (MS (num -> (num -> num)) (lambda (x) (lambda (y) y)))
  • Slides from the "Earth versus Mars" talk given by Jacob at Northeastern University.