Safe and Principled Language Interoperation

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2005
Accession Number
ADA436481

Entities

People

  • Valery Trifinov
  • Zhong Shao

Organizations

  • Yale University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Contracts
  • Environment
  • Governments
  • Information Operations
  • Language
  • Organizational Structure
  • Resource Management
  • Semantics
  • Social Sciences
  • Words (Language)

Fields of Study

  • Computer science
  • Engineering

Readers

  • Computational Linguistics
  • Cybersecurity.
  • Software Engineering.

Technology Areas

  • Space