A Calculus for Dynamic Linking

  • Davide Ancona
  • Sonia Fagorzi
  • Elena Zucca
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2841)


We define a calculus for modeling dynamic linking independently of the details of a particular programming environment.

The calculus distinguishes at the language level the notions of software configuration and execution, by introducing separate syntactic notions of linkset expression and command, respectively.

A reduction step can be either a simplification of a linkset expression, or the execution of a command w.r.t. a specific underlying software configuration denoted by a linkset expression; because of dynamic linking, these two kinds of reductions are interleaved.

The type system of the calculus, which is proved to be sound, relies on an accurate dependency analysis for ensuring type safety without losing the advantages offered by dynamic linking.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ancona, D., Fagorzi, S., Moggi, E., Zucca, E.: Mixin Modules and Computational Effects. In: International Colloquium on Automata, Languages and Programming 2003 (2003) (to appear)Google Scholar
  2. 2.
    Ancona, D., Zucca, E.: A calculus of module systems. Journ. of Functional Programming 12(2), 91–132 (2002)zbMATHMathSciNetGoogle Scholar
  3. 3.
    Bierman, G., Hicks, M., Sewell, P., Stoyle, G.: Formalizing dynamic software updating (extended abstract). In: USE 2003 - Workshop on Unexpected Software Evolution (2003)Google Scholar
  4. 4.
    Cardelli, L.: Program fragments, linking, and modularization. In: ACM Symp. on Principles of Programming Languages 1997, pp. 266–277. ACM Press, New York (1997)Google Scholar
  5. 5.
    Crary, K., Harper, R., Puri, S.: What is a recursive module. In: PLDI 1999 – ACM Conf. on Programming Language Design and Implementation (1999)Google Scholar
  6. 6.
    Drossopoulou, S.: Towards an abstract model of Java dynamic linking and verfication. In: Harper, R. (ed.) TIC 2000. LNCS, vol. 2071, pp. 53–84. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Drossopoulou, S., Eisenbach, S., Wragg, D.: A fragment calculus - towards a model of separate compilation, linking and binary compatibility. In: Proc. 14th Ann. IEEE Symp. on Logic in Computer Science (July 1999)Google Scholar
  8. 8.
    Drossopoulou, S., Lagorio, G., Eisenbach, S.: Flexible models for dynamic linking. In: European Symposium on Programming 2003 (2003)Google Scholar
  9. 9.
    Findler, R.B., Flatt, M.: Modular object-oriented programming with units and mixins. In: Intl. Conf. on Functional Programming 1998 (September 1998)Google Scholar
  10. 10.
    Gelernter, D., Carriero, N.: Coordination languages and their significance. Comm. ACM 35(1), 96–107 (1992)CrossRefGoogle Scholar
  11. 11.
    Hirschowitz, T., Leroy, X.: Mixin modules in a call-by-value setting. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 6–20. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Leroy, X.: A modular module system. Journal of Functional Programming 10(3), 269–303 (2000)zbMATHCrossRefGoogle Scholar
  13. 13.
    Machkasova, E., Turbak, F.A.: A calculus for link-time compilation. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 260–274. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  14. 14.
    Wells, J.B., Vestergaard, R.: Confluent equational reasoning for linking with first-class primitive modules. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 412–428. Springer, Heidelberg (2000)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Davide Ancona
    • 1
  • Sonia Fagorzi
    • 1
  • Elena Zucca
    • 1
  1. 1.DISIUniversità di GenovaGenovaItaly

Personalised recommendations