Jacob Matthews
Robert Bruce Findler
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.
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.
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.
- Abadi, M., Cardelli, L., Pierce, B., and Plotkin, G. 1991. Dynamic typing in a statically typed language. ACM Trans. Program. Lang. Syst. 13, 2, 237--268. Google Scholar
Digital Library
- Barzilay, E. and Clements, J. 2005. Laziness without all the hard work. In Workshop on Functional and Declarative Programming in Education (FDPE). Google ScholarDigital Library
- Barzilay, E. and Orlovsky, D. 2004. Foreign interface for PLT Scheme. In Proceedings of the Workshop on Scheme and Functional Programming.Google Scholar
- Beazley, D. 1996. SWIG: An easy to use tool for integrating scripting languages with C and C++. In Proceedings of the 4th Tcl/Tk Workshop. 129--139. Google ScholarDigital Library
- Beazley, D. 1997. Pointers, constraints, and typemaps. In SWIG 1.1 Users Manual.Google Scholar
- Benton, N. 2005. Embedded interpreters. J. Funct. Program. 15, 503--542. Google ScholarDigital Library
- Benton, N. and Kennedy, A. 1999. Interlanguage working without tears: Blending SML with Java. In ACM SIGPLAN International Conference on Functional Programming (ICFP). 126--137. Google ScholarDigital Library
- Benton, N., Kennedy, A., and Russo, C. V. 2004. Adventures in interoperability: the SML.NET experience. In Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP). 215--226. Google ScholarDigital Library
- Blume, M. 2001. No-longer-foreign: Teaching an ML compiler to speak C “natively”. In Proceedings of the Workshop on Multi-Language Infrastructure and Interoperability (BABEL).Google ScholarCross Ref
- Cardelli, L. 1986. Amber. In Combinators and functional programming languages, G. Cousineau, P.-L. Curien, and B. Robinet, Eds. Vol. 242. Springer-Verlag. Google ScholarDigital Library
- Chakravarty, M. M. T. 2002. The Haskell 98 foreign function interface 1.0.Google Scholar
- Chambers, C. and The Cecil Group. 2004. The Cecil language: Specification and rationale, version 3.2. Tech. rep., Department of Computer Science and Engineering, University of Washington. February.Google Scholar
- Felleisen, M. 1991. On the expressive power of programming languages. Sci. Comput. Program. 17, 35--75. Google ScholarDigital Library
- Felleisen, M., Friedman, D., Kohlbecker, E., and Duba, B. 1987. A syntactic theory of sequential control. Theoret. Comput. Sci., 205--237. Google ScholarDigital Library
- Felleisen, M. and Hieb, R. 1992. The revised report on the syntactic theories of sequential control and state. Theoret. Comput. Sci. 102, 235--271. Original version in: Technical Report 89-100, Rice University, June 1989.Google ScholarDigital Library
- Findler, R. B. and Blume, M. 2006. Contracts as pairs of projections. In Proceedings of the International Symposium on Functional and Logic Programming (FLOPS). Google ScholarDigital Library
- Findler, R. B. and Felleisen, M. 2002. Contracts for higher-order functions. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP). Google ScholarDigital Library
- Finne, S., Leijen, D., Meijer, E., and Peyton Jones, S. 1999. Calling Hell from Heaven and Heaven from Hell. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP). 114--125. Google ScholarDigital Library
- Fisher, K., Pucella, R., and Reppy, J. 2001. A framework for interoperability. In Proceedings of the Workshop on Multi-Language Infrastructure and Interoperability (BABEL).Google Scholar
- Flanagan, C. 2006. Hybrid type checking. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Furr, M. and Foster, J. S. 2005. Checking type safety of foreign function calls. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 62--72. Google ScholarDigital Library
- Furr, M. and Foster, J. S. 2008. Checking type safety of foreign function calls. ACM Trans. Program. Lang. Syst. 30, 4. Google ScholarDigital Library
- Girard, J.-Y., Lafont, Y., and Taylor, P. 1989. Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press. Google ScholarDigital Library
- Gordon, A. D. and Syme, D. 2001. Typing a multi-language intermediate code. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 248--260. Google ScholarDigital Library
- Gray, K. E., Findler, R. B., and Flatt, M. 2005. Fine grained interoperability through mirrors and contracts. In Proceedings of the Conference on Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA). Google ScholarDigital Library
- Grossman, D., Morrisett, G., and Zdancewic, S. 2000. Syntactic type abstraction. ACM Trans. Program. Lang. Syst. 22, 1037--1080. Google ScholarDigital Library
- Henglein, F. 1994. Dynamic typing: Syntax and proof theory. Sci. Comput. Program. 22, 3, 197--230. Google ScholarDigital Library
- Henglein, F. and Rehof, J. 1995. Safe polymorphic type inference for a dynamically typed language: translating Scheme to ML. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture (FPCA). Google ScholarDigital Library
- Ibrahim, R. and Szyperski, C. 1997. The COMEL language. Tech. Rep. FIT-TR-97-06, Faculty of Information Technology, Queensland University of Technology, Brisbane, Australia. Google ScholarDigital Library
- Kennedy, A. 2006. Securing the .NET programming model. Theoret. Comput. Sci. 364, 3, 311--317. Google ScholarDigital Library
- Kornstaedt, L. 2001. Alice in the land of Oz - an interoperability-based implementation of a functional language on top of a relational language. In Proceedings of the Workshop on Multi-Language Infrastructure and Interoperability (BABEL).Google ScholarCross Ref
- Mason, I. and Talcott, C. 1991. Equivalence in functional languages with effects. J. Funct. Program. 1, 287--327.Google ScholarCross Ref
- Matthews, J. 2008. Equation-preserving multi-language systems. Tech. Rep. TR-2008-06, University of Chicago.Google Scholar
- Matthews, J. and Ahmed, A. 2008. Parametric polymorphism through run-time sealing, or, theorems for low, low prices! In Proceedings of the European Symposium on Programming (ESOP). Google ScholarDigital Library
- Matthews, J. and Findler, R. B. 2007. Operational semantics for multi-language programs. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). Extended version appears as University of Chicago Technical Report TR-2007-8, under review. Google ScholarDigital Library
- Matthews, J., Findler, R. B., Flatt, M., and Felleisen, M. 2004. A visual environment for developing context-sensitive term rewriting systems. In Proceedings of the International Conference on Rewriting Techniques and Applications (RTA).Google Scholar
- Meijer, E., Perry, N., and van Yzendoorn, A. 2001. Scripting .NET using Mondrian. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP). Springer-Verlag, London, UK, 150--164. Google ScholarDigital Library
- Meunier, P. and Silva, D. 2003. From Python to PLT Scheme. In Proceedings of the 4th Workshop on Scheme and Functional Programming. 24--29.Google Scholar
- Odersky, M., Altherr, P., Cremet, V., Emir, B., Micheloud, S., Mihaylov, N., Schinz, M., Stenman, E., and Zenger, M. 2005. An Introduction to Scala. http://scala.epfl.ch/docu/files/ScalaIntro.pdf.Google Scholar
- Ohori, A. and Kato, K. 1993. Semantics for communication primitives in an polymorphic language. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 99--112. Google ScholarDigital Library
- Pierce, B. and Sumii, E. 2000. Relating cryptography and polymorphism. Unpublished manuscript.Google Scholar
- Pierce, B. C. 2002. Types and Programming Languages. The MIT Press. Google ScholarDigital Library
- Pinto, P. 2003. Dot-Scheme: A PLT Scheme FFI for the .NET framework. In Proceedings of the Workshop on Scheme and Functional Programming.Google Scholar
- Plotkin, G. D. 1977. LCF considered as a programming language. Theor. Comput. Sci. 223--255.Google Scholar
- Pucella, R. 2002. Towards a formalization for COM, part I: The primitive calculus. In Proceedings of the Conference on Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA). Google ScholarDigital Library
- Ramsey, N. 2003. Embedding an interpreted language using higher-order functions and types. In Proceedings of the Conference on Interpreters, Virtual Machines and Emulators (IVME '03). 6--14. Google ScholarDigital Library
- Reynolds, J. C. 1983. Types, abstraction and parametric polymorphism. In Proceedings of the IFIP Congress. 513--523.Google Scholar
- Sabry, A. and Felleisen, M. 1993. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation. Google ScholarDigital Library
- Steckler, P. 1999. MysterX: A Scheme toolkit for building interactive applications with COM. In Technology of Object-Oriented Languages and Systems (TOOL). 364--373. Google ScholarDigital Library
- Sumii, E. and Pierce, B. 2003. Logical relations for encryption. J. Comput. Secur. 11, 4, 521--554. Google ScholarDigital Library
- Sumii, E. and Pierce, B. 2004. A bisimulation for dynamic sealing. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Tait, W. 1967. Intensional interpretations of functionals of finite type I. J. Symb. Log. 32, 2, 198--212.Google ScholarCross Ref
- Trifonov, V. and Shao, Z. 1999. Safe and principled language interoperation. In Proceedings of the European Symposium on Programming (ESOP). 128--146. Google ScholarDigital Library
- Wright, A. and Felleisen, M. 1994. A syntactic approach to type soundness. Information and Computation, 38--94. First appeared as Tech. Rep. TR160, Rice University, 1991. Google ScholarDigital Library
- Zdancewic, S., Grossman, D., and Morrisett, G. 1999. Principals in programming languages. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP). Google ScholarDigital Library
Index Terms
- Operational semantics for multi-language programs
Recommendations
Operational semantics for multi-language programs
POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesInter-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 ...
Operational semantics for multi-language programs
Proceedings of the 2007 POPL ConferenceInter-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 ...
Formalisation of C Language Interfaces
In practical computing, implementations of programming languages provide an interface that allow programs written in a language to call code written in another programming language, most often C. Usually, those language interfaces are left out of the ...
Comments