Skip to main content
A Calculus for Dynamic Loading
Technical Reports (CIS)
  • Michael Hicks, University of Pennsylvania
  • Stephanie C Weirich, University of Pennsylvania
Document Type
Technical Report
Date of this Version
University of Pennsylvania Department of Computer and Information Science Technical Report No. MS-CIS-00-07.

At the time of publication, the author Stephanie C. Weirich was affiliated with Cornell University. Currently June 2007, she is a faculty member in the Department of Computer Information and Science at the University of Pennsylvania.

We present the load-calculus, used to model dynamic loading, and prove it 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 the process of dynamic loading in TAL/Load [4], a version of Typed Assembly Language [7] extending with dynamic linking. To model the key aspects of TAL, the calculus contains references and facilities for named types. Loadable programs may refer to named types defined by the running program, and may export new types to code loaded later. Our approach follows the framework initially outlined by Glew et. al [3]. This calculus has been implemented in the TALx86 [6] version of Typed Assembly Language, and is used to implement a full-featured dynamic linking library, DLpop [4].

Citation Information
Michael Hicks and Stephanie C Weirich. "A Calculus for Dynamic Loading" (2001)
Available at: