Abstract
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.
Partially supported by Dynamic Assembly, Reconfiguration Type-checking – EC project IST-2001-33477, APPSEM II – Thematic network IST-2001-38957, and Murst NAPOLI – Network Aware Programming: Oggetti, Linguaggi, Implementazioni.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Ancona, D., Zucca, E.: A calculus of module systems. Journ. of Functional Programming 12(2), 91–132 (2002)
Bierman, G., Hicks, M., Sewell, P., Stoyle, G.: Formalizing dynamic software updating (extended abstract). In: USE 2003 - Workshop on Unexpected Software Evolution (2003)
Cardelli, L.: Program fragments, linking, and modularization. In: ACM Symp. on Principles of Programming Languages 1997, pp. 266–277. ACM Press, New York (1997)
Crary, K., Harper, R., Puri, S.: What is a recursive module. In: PLDI 1999 – ACM Conf. on Programming Language Design and Implementation (1999)
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)
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)
Drossopoulou, S., Lagorio, G., Eisenbach, S.: Flexible models for dynamic linking. In: European Symposium on Programming 2003 (2003)
Findler, R.B., Flatt, M.: Modular object-oriented programming with units and mixins. In: Intl. Conf. on Functional Programming 1998 (September 1998)
Gelernter, D., Carriero, N.: Coordination languages and their significance. Comm. ACM 35(1), 96–107 (1992)
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)
Leroy, X.: A modular module system. Journal of Functional Programming 10(3), 269–303 (2000)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ancona, D., Fagorzi, S., Zucca, E. (2003). A Calculus for Dynamic Linking. In: Blundo, C., Laneve, C. (eds) Theoretical Computer Science. ICTCS 2003. Lecture Notes in Computer Science, vol 2841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45208-9_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-45208-9_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20216-5
Online ISBN: 978-3-540-45208-9
eBook Packages: Springer Book Archive