Safe and Principled Language Interoperation
Last modified: Tue Mar 14 19:32:35 2000 GMT.
Safety of interoperation of program fragments written in different safe languages may fail when the languages have different systems of computational effects: an exception raised by an ML function may have no valid semantic interpretation in the context of a Safe-C caller. Sandboxing costs performance and still may violate the semantics if effects are not taken into account. We show that effect annotations alone are insufficient to guarantee safety, and we present a type system with bounded effect polymorphism designed to verify the compatibility of abstract resources required by the computational models of the interoperating languages. The type system ensures single address space interoperability of statically typed languages with effect mechanisms built of modules for control and state. It is shown sound for safety with respect to the semantics of a language with constructs for selection, simulation, and blocking of resources, targeted as an intermediate language for optimization of resource handling.
To appear in Proc. 1999 European Symposium on Programming (ESOP'99), Amsterdam, The Netherlands, March 1999. Lecture Notes in Computer Science, Springer-Verlag.
TextGzipped Postscript [86k]
Copyright © 1996-2021 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science