Equation-preserving multilanguage systems

Jacob Matthews. 25 April, 2008.
Communicated by Robby Findler.


Kennedy has recently argued that the designers of Cshould try to informally verify that their compilation from C♯ source to Microsoft Common Language Run- time (CLR) bytecode is “fully abstract” in the sense that any two code fragments that C♯ programs cannot distinguish must compile into CLR code fragments that CLR programs also cannot distinguish. In this paper we treat that property as a criterion for what constitutes a well-designed interoperability system and refine it using the techniques of Matthews-Findler-style multilanguage systems. We begin by giving our own variation on Kennedy’s criterion that does not directly involve a notion of compilation. Then we argue that our criterion is useful and workable by using it to guide our development of a multilanguage system that combines call-by-name and call-by-value lambda calculi. We begin with a straightforward system that we show does not meet our criterion. Then we refine that system’s interoperability rules and show that the result does meet our criterion. We con- clude by sketching how our criterion would apply to multilanguage systems whose constituent languages had more advanced features such as state, exceptions, and concurrent threads.

Original Document

The original document is available in PDF (uploaded 25 April, 2008 by Robby Findler).