Hostname: page-component-586b7cd67f-l7hp2 Total loading time: 0 Render date: 2024-11-22T06:59:54.988Z Has data issue: false hasContentIssue false
  • English
  • Français

A calculus of open modules: call-by-need strategy and confluence†

Published online by Cambridge University Press:  01 August 2007

SONIA FAGORZI  and
ELENA ZUCCA
SONIA FAGORZI
Affiliation:
Dipartimento di Informatica e Scienze dell'Informazione, Università di Genova, Via Dodecaneso, 35, 16146 Genova, Italy Email: [email protected], [email protected]
ELENA ZUCCA
Affiliation:
Dipartimento di Informatica e Scienze dell'Informazione, Università di Genova, Via Dodecaneso, 35, 16146 Genova, Italy Email: [email protected], [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We present a simple module calculus where selection and execution of a component is possible on open modules, that is, modules that still need to import some external definitions. Hence, it provides a kernel model for a computational paradigm in which standard execution (that is, execution of a single computation described by a fragment of code) can be interleaved with operations at the meta-level, which can manipulate in various ways the context in which this computation takes place. Formally, this is achieved by introducing configurations as basic terms. These are, roughly speaking, pairs consisting of an (open, mutually recursive) collection of named components and a term representing a program running in the context of these components. Configurations can be manipulated by classical module/fragment operators, hence reduction steps can be either execution steps of the program or steps that perform module operations (called reconfiguration steps).

Since configurations combine the features of lambda abstractions (first-class functions), records, environments with mutually recursive definitions and modules, the calculus extends and integrates both traditional module calculi and recursive lambda calculi. We state confluence of the calculus, and propose different ways to prevent errors arising from the lack of some required component, either by a purely static type system or by a combination of static and run-time checks. Moreover, we define a call-by-need strategy that performs module simplification only when needed and only once, leading to a generalisation of call-by-need lambda calculi that includes module features. We prove the soundness and completeness of this strategy using an approach based on information content, which also allows us to preserve confluence, even when local substitution rules are added to the calculus.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 17 , Issue 4 , August 2007 , pp. 675 - 751
Copyright
Copyright © Cambridge University Press 2007

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abadi, M. and Cardelli, L. (1996) A Theory of Objects, Monographs in Computer Science, Springer.CrossRefGoogle Scholar
Abadi, M., Gonthier, G. and Werner, B. (2004) Choice in dynamic linking. In: FOSSACS'04 – Foundations of Software Science and Computation Structures 2004. Springer-Verlag Lecture Notes in Computer Science 2987 12–26.CrossRefGoogle Scholar
Ancona, D. (1998) Modular Formal Frameworks for Module Systems, Ph.D. thesis, Dipartimento di Informatica, Università di Pisa.Google Scholar
Ancona, D., Fagorzi, S. and Zucca, E. (2003) A calculus for dynamic linking. In: Blundo, C. and Laneve, C. (eds.) Italian Conference on Theoretical Computer Science 2003. Springer-Verlag Lecture Notes in Computer Science 2841 284–301.CrossRefGoogle Scholar
Ancona, D., Fagorzi, S. and Zucca, E. (2004) A calculus with lazy module operators. In: Lévy, J. -J., Mayr, E. W. and Mitchell, J. C. (eds.) TCS 2004 (IFIP International Conference on Theoretical Computer Science), Kluwer Academic Publishers 423–436.Google Scholar
Ancona, D., Fagorzi, S. and Zucca, E. (2005a) A calculus for dynamic reconfiguration with low priority linking. In: WOOD'04 – Workshop on Object-Oriented Development. Electronic Notes in Theoretical Computer Science 138 (2)3–35.CrossRefGoogle Scholar
Ancona, D., Fagorzi, S. and Zucca, E. (2005b) Mixin modules for dynamic rebinding. In: De, Nicola R. and Sangiorgi, D. (eds.) TGC 2005 – Trustworthy Global Computing. Springer-Verlag Lecture Notes in Computer Science 3705 279–298.CrossRefGoogle Scholar
Ancona, D. and Zucca, E. (1998) A theory of mixin modules: Basic and derived operators. Mathematical Structures in Computer Science 8 (4)401–446.CrossRefGoogle Scholar
Ancona, D. and Zucca, E. (1999) A primitive calculus for module systems. In: Nadathur, G. (ed.) PPDP'99 – Principles and Practice of Declarative Programming. Springer-Verlag Lecture Notes in Computer Science 1702 62–79.CrossRefGoogle Scholar
Ancona, D. and Zucca, E. (2002) A calculus of module systems. Journal of Functional Programming 12 (2)91–132.CrossRefGoogle Scholar
Ariola, Z. M. and Blom, S. (1997) Cyclic lambda calculi. In: Abadi, M. and Ito, T. (eds.) Theoretical Aspects of Computer Software. Springer-Verlag Lecture Notes in Computer Science 1281 77–106.CrossRefGoogle Scholar
Ariola, Z. M. and Blom, S. (2002) Skew confluence and the lambda calculus with letrec. Annals of Pure and Applied Logic 117 (1-3)95–168.CrossRefGoogle Scholar
Ariola, Z. M. and Felleisen, M. (1997) The call-by-need lambda calculus. Journal of Functional Programming 7 (3)265–301.CrossRefGoogle Scholar
Ariola, Z. M. and Klop, J. W. (1997) Lambda calculus with explicit recursion. Information and Computation 139 (2)154–233.CrossRefGoogle Scholar
Bettini, L., Venneri, B. and Bono, V. (2005) MOMI: a calculus for mobile mixins. Acta Informatica 42 (2-3)143–190.CrossRefGoogle Scholar
Bierman, G., Hicks, M. W., Sewell, P., Stoyle, G. and Wansbrough, K. (2003) Dynamic rebinding for marshalling and update, with destruct-time λ. In Runciman, C. and Shivers, O. (eds.) International Conference on Functional Programming 2003, ACM Press 99–110.Google Scholar
Buckley, A., Murray, M., Eisenbach, S. and Drossopoulou, S. (2005) Flexible bytecode for linking in .NET. Electronic Notes in Theoretical Computer Science 141 (1)75–92.CrossRefGoogle Scholar
Drossopoulou, S. (2001) Towards an abstract model of Java dynamic linking and verification. In: Harper, R. (ed.) TIC'00 – Third Workshop on Types in Compilation (Selected Papers). Springer-Verlag Lecture Notes in Computer Science 2071 53–84.CrossRefGoogle Scholar
Drossopoulou, S., Lagorio, G. and Eisenbach, S. (2003) Flexible models for dynamic linking. In: Degano, P. (ed.) ESOP 2003 – European Symposium on Programming 2003. Springer-Verlag Lecture Notes in Computer Science 2618 38–53.CrossRefGoogle Scholar
Drossopoulou, S., Lagorio, G. and Eisenbach, S. (2006) A flexible model for dynamic linking in Java and C#. Theoretical Computer Science (to appear).Google Scholar
Fagorzi, S. (2005) Module Calculi for Dynamic Reconfiguration, Ph.D. thesis, Dipartimento di Informatica e Scienze dell'Informazione, Università di Genova.Google Scholar
Fagorzi, S. and Zucca, E. (2004) A case-study in encoding configuration languages: Multiple class loaders. Journal of Object Technology 3 (11)31–53.CrossRefGoogle Scholar
Fagorzi, S. and Zucca, E. (2005) A calculus for reconfiguration. In: DCM 2005 – International Workshop on Developments in Computational Models. Electronic Notes in Theoretical Computer Science 135 (3).Google Scholar
Fagorzi, S. and Zucca, E. (2006a) A calculus of components with dynamic type-checking. In: Formal Aspects of Component Software (FACS'06). Electronic Notes in Theoretical Computer Science (to appear).CrossRefGoogle Scholar
Fagorzi, S. and Zucca, E. (2006b) A framework for type safe exchange of mobile code. In: TGC 2006 – Trustworthy Global Computing. Springer-Verlag Lecture Notes in Computer Science (to appear).Google Scholar
Fagorzi, S. and Zucca, E. (2006c) A framework for type safe exchange of mobile code. Technical report, Dipartimento di Informatica e Scienze dell'Informazione, Università di Genova. (Extended version of Fagorzi and Zucca (2006)b).Google Scholar
Felleisen, M. and Friedman, D. P. (1986) Control operators, the SECD-machine, and the lambda calculus. In: 3rd Working Conference on the Formal Description of Programming Concepts, Ebberup, Denmark 193–219.Google Scholar
Hicks, M. W., Moore, J. and Nettles, S. (2001) Dynamic software updating. In: PLDI'01 – ACM Conference on Programming Language Design and Implementation, ACM Press.Google Scholar
Hicks, M. W. and Nettles, S. (2005) Dynamic software updating. ACM Transactions on Programming Languages and Systems 27 (6)1049–1096.CrossRefGoogle Scholar
Hindley, J. R. (1964) The Church–Rosser Property and a Result in Combinatory Logic, Ph.D. thesis, University of Newcastle-upon-Tyne.Google Scholar
Hirschowitz, T. (2004) Rigid mixin modules. In: Kameyama, Y. and Stuckey, P. J. (eds.) FLOPS 2004 – Functional and Logic Programming. Springer-Verlag Lecture Notes in Computer Science 2998 214–228.CrossRefGoogle Scholar
Hirschowitz, T. and Leroy, X. (2002) Mixin modules in a call-by-value setting. In: Le Métayer, D. (ed.) ESOP 2002 – European Symposium on Programming 2002. Springer-Verlag Lecture Notes in Computer Science 2305 6–20.CrossRefGoogle Scholar
Hirschowitz, T., Leroy, X. and Wells, J. B. (2004) Call-by-value mixin modules: Reduction semantics, side effects, types. In: Schmidt, D. A. (ed.) ESOP 2003 – European Symposium on Programming 2003. Springer-Verlag Lecture Notes in Computer Science 2986 64–78.CrossRefGoogle Scholar
Klop, J. (1987) Term rewriting systems: a tutorial. Bulletin of EATCS 32 143–182.Google Scholar
Klop, J., van Oostrom, V. and van Raamsdonk, F. (1993) Combinatory reduction systems: introduction and survey. Technical Report CS-R9362, CWI.CrossRefGoogle Scholar
Lagorio, G. (2006) Dynamic linking of polymorphic bytecode. In: 8th International Workshop on Formal Techniques for Java-like Programs.Google Scholar
Liu, Y. D. and Smith, S. F. (2004) Modules with interfaces for dynamic linking and communication. In: Odersky, M. (ed.) ECOOP'04 – Object-Oriented Programming. Springer-Verlag Lecture Notes in Computer Science 3086 414–439.Google Scholar
Machkasova, E. and Turbak, F. (2000) A calculus for link-time compilation. In: ESOP 2000 – European Symposium on Programming 2000. Springer-Verlag Lecture Notes in Computer Science 1782 260–274.CrossRefGoogle Scholar
Makholm, H. and Wells, J. B. (2005) Type inference, principal typings, and let-polymorphism for first-class mixin modules. In: Danvy, O. and Pierce, B. C. (eds.) International Conference on Functional Programming 2005, ACM Press 156–167.Google Scholar
Mens, T. and Kniesel, G. (2004) Workshop on foundations of unanticipated software evolution. ETAPS 2004 (available at http://joint.org/fuse2004/).Google Scholar
Moreau, L. (1998) A syntactic theory of dynamic binding. Higher-Order and Symbolic Computation 11 (3)233–279.CrossRefGoogle Scholar
Stoyle, G., Hicks, M. W., Bierman, G., Sewell, P. and Neamtiu, I. (2005) Mutatis mutandis: safe and predictable dynamic software updating. In: ACM Symposium on Principles of Programming Languages 2005, ACM Press 183–194.Google Scholar
van Oostrom, V. (1994) Confluence for Abstract and Higher-Order Rewriting, Ph.D. thesis, Vrije Universiteit, Amsterdam.Google Scholar
Wells, J. B. and Vestergaard, R. (2000) Confluent equational reasoning for linking with first-class primitive modules. In: ESOP 2000 – European Symposium on Programming 2000. Springer-Verlag Lecture Notes in Computer Science 1782 412–428.CrossRefGoogle Scholar