Research

People

Publications

Software

Support

Links

Internal

Safe and Principled Language Interoperation

Last modified: Tue Mar 14 19:32:35 2000 GMT.

Authors

Abstract

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.

Published

To appear in Proc. 1999 European Symposium on Programming (ESOP'99), Amsterdam, The Netherlands, March 1999. Lecture Notes in Computer Science, Springer-Verlag.

Text