|
Abstract : |
A calculus for dynamic loading is presented and proved sound. The calculus extends the polymorphic -calculus with a load primitive that dynamically loads terms that are closed, with respect to values. The calculus is meant to approximate Typed Assembly Language [3], and thus contains references, and facilities for generative types. Loadable programs may refer to generative types dened by the running program, and may export new types to code loaded later. Our approach follows the framework initially outlined by Glew et. al [1]. This calculus has been implemented in the TALx86 [4] version of Typed Assembly Language, and forms the foundation of a exible and ecient approach to dynamic linking therein. 1, |
