Entry Matthews:2009:OSM from toplas.bib

Last update: Tue May 1 02:05:46 MDT 2012                Valid HTML 3.2!

Index sections

Top | Symbols | Math | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

BibTeX entry

@Article{Matthews:2009:OSM,
  author =       "Jacob Matthews and Robert Bruce Findler",
  title =        "Operational semantics for multi-language programs",
  journal =      j-TOPLAS,
  volume =       "31",
  number =       "3",
  pages =        "12:1--12:44",
  month =        apr,
  year =         "2009",
  CODEN =        "ATPSDT",
  DOI =          "http://doi.acm.org/10.1145/1498926.1498930",
  ISSN =         "0164-0925 (print), 1558-4593 (electronic)",
  ISSN-L =       "0164-0925",
  bibdate =      "Thu Apr 16 14:08:54 MDT 2009",
  bibsource =    "http://www.acm.org/pubs/contents/journals/toplas/;
                 http://www.math.utah.edu/pub/tex/bib/toplas.bib",
  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 --- for instance,
                 SML.NET, F\#, Mondrian, and Scala all treat
                 interoperability as a central design feature. Still,
                 current multi-language research tends not to focus on
                 the semantics of these features, but only on how to
                 implement them efficiently. In this article, we attempt
                 to rectify that by giving a technique for specifying
                 the operational semantics of 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, equivalence, and
                 termination behavior. In doing so it allows us to adapt
                 standard theoretical techniques such as
                 subject-reduction, logical relations, and operational
                 equivalence for use on multi-language systems.
                 Generally speaking, our proofs of properties in a
                 multi-language context are mutually referential
                 versions of their single language counterparts.\par

                 We demonstrate our technique with a series of
                 strategies for embedding a Scheme-like language into an
                 ML-like language. We start by connecting very simple
                 languages with a very simple strategy, and work our way
                 up to languages that interact in sophisticated ways and
                 have sophisticated features such as polymorphism and
                 effects. Along the way, we prove relevant results such
                 as type-soundness and termination for each system we
                 present using adaptations of standard
                 techniques.\par

                 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.",
  acknowledgement = ack-nhfb,
  articleno =    "12",
  fjournal =     "ACM Transactions on Programming Languages and
                 Systems",
  keywords =     "interoperability; Operational semantics",
}

Related entries