Type-safe Linking and Modular Assembly Language

DSpace/Manakin Repository

Type-safe Linking and Modular Assembly Language

Citable link to this page


Title: Type-safe Linking and Modular Assembly Language
Author: Glew, Neal; Morrisett, John Gregory

Note: Order does not necessarily reflect citation order of authors.

Citation: Glew, Neal, and Greg Morrisett. Type-safe linking and modular assembly language. In POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 250-261, New York, NY, USA, 1999. ACM
Full Text & Related Files:
Abstract: Linking is a low-level task that is usually vaguely specified, if at all, by language definitions. However, the security of web browsers and other extensible systems depends crucially upon a set of checks that must be performed at link time. Building upon the simple, but elegant ideas of Cardelli, and module constructs from high-level languages, we present a formal model of typed object files and a set of inference rules that are sufficient to guarantee that type safety is preserved by the linking process.

Whereas Cardelli's link calculus is built on top of the simply-typed lambda calculus, our object files are based upon typed assembly language so that we may model important low-level implementation issues. Furthermore, unlike Cardelli, we provide support for abstract types and higher-order type constructors - features critical for building extensible systems or modern programming languages such as ML.
Published Version: http://doi.acm.org/10.1145/292540.292563
Terms of Use: This article is made available under the terms and conditions applicable to Other Posted Material, as set forth at http://nrs.harvard.edu/urn-3:HUL.InstRepos:dash.current.terms-of-use#LAA
Citable link to this page: http://nrs.harvard.edu/urn-3:HUL.InstRepos:2797448
Downloads of this work:

Show full Dublin Core record

This item appears in the following Collection(s)


Search DASH

Advanced Search