Type-Safe Linking and Modular Assembly Language

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 higherorder type constructors—features critical for building extensible systems or modern programming languages such as ML.

• Type: Conference
• Year: 1999
• Where: POPL
• Authors: Neal Glew, J. Gregory Morrisett
• Keywords: Cardelli’s Link Calculus, Extensible Systems, Object files, POPL 1999, Programming Languages