TR-2008-06
Equation-preserving multilanguage systems
Jacob Matthews. 25 April, 2008.
Communicated by Robby Findler.
Abstract
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).
