Operational semantics for multi-language programs

ABSTRACT

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.

REFERENCES

• 1: Martín Abadi , Luca Cardelli , Benjamin Pierce , Gordon Plotkin, Dynamic typing in a statically typed language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.2, p.237-268, April 1991 [doi>10.1145/103135.103138]
• 2: Eli Barzilay , John Clements, Laziness without all the hard work: combining lazy and strict languages for teaching, Proceedings of the 2005 workshop on Functional and declarative programming in education, September 25-25, 2005, Tallinn, Estonia [doi>10.1145/1085114.1085118]
• 3: E. Barzilay and D. Orlovsky. Foreign interface for PLT Scheme. In Workshop on Scheme and Functional Programming, 2004.
• 4: D. Beazley. Pointers, constraints, and typemaps. In SWIG 1.1 Users Manual. Available online: http://www.swig.org/Doc1.1/HTML/Typemaps.html.
• 5: D. Beazley. SWIG: An easy to use tool for integrating scripting languages with C and C++. In 4th Tcl/Tk Workshop, pages 129--139, 1996. Available online: http://www.swig.org/papers/Tcl96/tcl96.html.
• 6: Nick Benton, Embedded interpreters, Journal of Functional Programming, v.15 n.4, p.503-542, July 2005 [doi>10.1017/S0956796804005398]
• 7: Nick Benton , Andrew Kennedy, Interlanguage working without tears: blending SML with Java, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.126-137, September 27-29, 1999, Paris, France
• 8: Nick Benton , Andrew Kennedy , Claudio V. Russo, Adventures in interoperability: the SML.NET experience, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.215-226, August 24-26, 2004, Verona, Italy [doi>10.1145/1013963.1013987]
• 9: M. Blume. No-longer-foreign: Teaching an ML compiler to speak C "natively". In Workshop on Multi-Language Infrastructure and Interoperability (BABEL), 2001.
• 10: L Cardelli, Amber, Proc. of the thirteenth spring school of the LITP on Combinators and functional programming languages, p.21-47, October 1986, Val d'Ajol, France
• 11: Manuel M. T. Chakravarty, C -> HASKELL, or Yet Another Interfacing Tool, Selected Papers from the 11th International Workshop on Implementation of Functional Languages, p.131-148, September 07-10, 1999
• 12: M. M. T. Chakravarty. The Haskell 98 foreign function interface 1.0, 2002. Available online: http://www.cse.unsw.edu.au/~chak/haskell/ffi/.
• 13: C. Chambers and The Cecil Group. The Cecil language: Specification and rationale, version 3.2. Technical report, Department of Computer Science and Engineering, University of Washington, February 2004. Available online: http://www.cs.washington.edu/research/projects/cecil/pubs/cecil-spec.html.
• 14: Matthias Felleisen, On the expressive power of programming languages, Science of Computer Programming, v.17 n.1-3, p.35-75, Dec. 1991
• 15: M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 102:235--271, 1992. Original version in: Technical Report 89--100, Rice University, June 1989.
• 16: R. B. Findler and M. Blume. Contracts as pairs of projections. In International Symposium on Functional and Logic Programming (FLOPS), 2006.
• 17: Robert Bruce Findler , Matthias Felleisen, Contracts for higher-order functions, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.48-59, October 04-06, 2002, Pittsburgh, PA, USA
• 18: Sigbjorn Finne , Daan Leijen , Erik Meijer , Simon Peyton Jones, Calling hell from heaven and heaven from hell, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.114-125, September 27-29, 1999, Paris, France
• 19: K. Fisher, R. Pucella, and J. Reppy. A framework for interoperability. In Workshop on Multi-Language Infrastructure and Interoperability (BABEL), 2001.
• 20: Cormac Flanagan, Hybrid type checking, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-256, January 11-13, 2006, Charleston, South Carolina, USA
• 21: Michael Furr , Jeffrey S. Foster, Checking type safety of foreign function calls, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 22: Andrew D. Gordon , Don Syme, Typing a multi-language intermediate code, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.248-260, January 2001, London, United Kingdom
• 23: Kathryn E. Gray , Robert Bruce Findler , Matthew Flatt, Fine-grained interoperability through mirrors and contracts, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 24: Fritz Henglein, Dynamic typing: syntax and proof theory, Science of Computer Programming, v.22 n.3, p.197-230, June 1994
• 25: Fritz Henglein , Jakob Rehof, Safe polymorphic type inference for a dynamically typed language: translating Scheme to ML, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.192-203, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224203]
• 26: R. Ibrahim , C. Szyperski, The COMEL Language, University of Queensland, 1997
• 27: Jython. http://www.jython.org/.
• 28: A. Kennedy. Securing the .NET programming model. Theoretical Computer Science, To appear. http://research.microsoft.com/~akenn/sec/.
• 29: L. Kornstaedt. Alice in the land of Oz - an interoperability-based implementation of a functional language on top of a relational language. In Workshop on Multi-Language Infrastructure and Interoperability (BABEL), 2001.
• 30: J. Matthews and R. B. Findler. An operational semantics for R5RS Scheme. In Workshop on Scheme and Functional Programming, 2005.
• 31: J. Matthews, R. B. Findler, M. Flatt, and M. Felleisen. A visual en-vironment for developing context-sensitive term rewriting systems. In Proceedings of the International Conference on Rewriting Techniques and Applications (RTA), 2004.
• 32: Erik Meijer , Nigel Perry , Arjan van Yzendoorn, Scripting .NET Using Mondrian, Proceedings of the 15th European Conference on Object-Oriented Programming, p.150-164, June 18-22, 2001
• 33: P. Meunier and D. Silva. From Python to PLT Scheme. In Proceedings of the Fourth Workshop on Scheme and Functional Programming, pages 24--29, 2003.
• 34: M. Odersky, P. Altherr, V. Cremet, B. Emir, S. Micheloud, N. Mihaylov, M. Schinz, E. Stenman, and M. Zenger. An Introduction to Scala. http://scala.epfl.ch/docu/files/ScalaIntro.pdf, 2005.
• 35: Atsushi Ohori , Kazuhiko Kato, Semantics for communication primitives in a polymorphic language, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.99-112, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158529]
• 36: P. Pinto. Dot-Scheme: A PLT Scheme FFI for the .NET framework. In Workshop on Scheme and Functional Programming, November 2003.
• 37: G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, pages 223--255, 1977.
• 38: Riccardo Pucella, Towards a formalization for COM part i: the primitive calculus, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 39: Norman Ramsey, Embedding an interpreted language using higher-order functions and types, Proceedings of the 2003 workshop on Interpreters, virtual machines and emulators, p.6-14, June 12-12, 2003, San Diego, California [doi>10.1145/858570.858571]
• 40: John Reppy , Chunyan Song, Application-specific foreign-interface generation, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA [doi>10.1145/1173706.1173714]
• 41: Paul A. Steckler, MysterX: A Scheme Toolkit for Building Interactive Applications with COM, Proceedings of the Technology of Object-Oriented Languages and Systems, p.364, August 01-05, 1999
• 42: Valery Trifonov , Zhong Shao, Safe and Principled Language Interoperation, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.128-146, March 22-28, 1999
• 43: A. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, pages 38--94, 1994. First appeared as Technical Report TR160, Rice University, 1991.
• 44: Steve Zdancewic , Dan Grossman , Greg Morrisett, Principals in programming languages: a syntactic proof technique, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.197-207, September 27-29, 1999, Paris, France

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

General Terms:
Languages, Theory

Keywords:
interoperability, multi-language systems, operational semantics