Abstract
Modules and linking are usually formalized by encodings which use the λ-calculus, records (possibly dependent), and possibly some construct for recursion. In contrast, we introduce the m-calculus, a calculus where the primitive constructs are modules, linking, and the selection and hiding of module components. The m-calculus supports smooth encodings of software structuring tools such as functions (λ-calculus), records, objects (ς-calculus), and mutually recursive definitions. The m-calculus can also express widely varying kinds of module systems as used in languages like C, Haskell, and ML. We prove the m-calculus is confluent, thereby showing that equational reasoning via the m-calculus is sensible and well behaved.
Supporting grants: EPSRC GR/L 36963, NSF CCR-9417382 and CCR-9806747.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Haskell 98: A non-strict, purely functional language. Technical report, The Haskell 98 Committee, 1 Feb. 1999. Currently available at http://haskell.org.
LNCS. Springer-Verlag, 2000.
M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag, 1996.
D. Ancona and E. Zucca. An algebra of mixin modules. In F. P. Presicce, editor, Recent Trends in Algebraic Development Techniques (12th Int’l Workshop, WADT’ 97 — Selected Papers), number 1376 in LNCS, pages 92–106. Springer-Verlag, 1998.
D. Ancona and E. Zucca. A primitive calculus for module systems. In G. Nadathur, editor, Proc. Int’l Conf. on Principles and Practice of Declarative Programming, LNCS, Paris, France, 29 Sept.–1 Oct. 1999. Springer-Verlag.
Z. M. Ariola and S. Blom. Cyclic lambda calculi. In Theoretical Aspects Comput. Softw.: Int’l Conf., 1997.
Z. M. Ariola and S. Blom. Lambda calculi plus letrec. Submitted, 3 July 1997.
Z. M. Ariola and J. W. Klop. Lambda calculus with explicit recursion. Inf. & Comput., 139:154–233, 1997.
H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, revised edition, 1984.
J. G. P. Barnes. Programming in Ada 95. Addison-Wesley, 1996.
V. Bono, M. Bugliesi, M. Dezani-Ciancaglini, and L. Liquori. Subtyping constraints for incomplete objects. Fundamenta Informaticae, 199X. To appear.
G. Bracha. The Programming Language Jigsaw: Mixins, Modularity, and Multiple Inheritance. PhD thesis, Univ. of Utah, Mar. 1992.
G. Bracha and G. Lindstrom. Modularity meets inheritance. In Proc. Int’l Conf. Computer Languages, pages 282–290, 1992.
L. Cardelli. Program fragments, linking, and modularization. In Conf. Rec. POPL’ 97: 24th ACM Symp. Princ. of Prog. Langs., 1997.
K. Crary, R. Harper, and S. Puri. What is a recursive module? In Proc. ACM SIGPLAN’ 99 Conf. Prog. Lang. Design & Impl., 1997.
S. Drossopoulou, S. Eisenbach, and D. Wragg. A fragment calculus — towards a model of separate compilation, linking and binary compatibility. In Proc. 14th Ann. IEEE Symp. Logic in Computer Sci., July 1999.
D. Duggan and C. Sourelis. Mixin modules. In Proc. 1996 Int’l Conf. Functional Programming, pages 262–273, 1996.
D. Duggan and C. Sourelis. Parameterized modules, recursive modules, and mixin modules. In ACM SIGPLAN Workshop on ML and its Applications, 1998.
R. B. Findler and M. Flatt. Modular object-oriented programming with units and mixins. In Proc. 1998 Int’l Conf. Functional Programming, 1998.
K. Fisher, F. Honsell, and J. C. Mitchell. A lambda calculus of objects and method specialization. Nordic Journal of Computing, 1(1):3–37, 1994.
M. Flatt and M. Felleisen. Units: Cool modules for HOT languages. In Proc. ACM SIGPLAN’ 98 Conf. Prog. Lang. Design & Impl., 1998.
M. Flatt, S. Krishnamurthi, and M. Felleisen. Classes and mixins. In Conf. Rec. POPL’ 98: 25th ACM Symp. Princ. of Prog. Langs., 1998.
B. R. Gaster and M. P. Jones. A polymorphic type system for extensible records and variants. Technical Report NOTTCS-TR-96-3, Univ. of Nottingham, 1996.
N. Glew and G. Morrisett. Type-safe linking and modular assembly language. In POPL’ 99 [38].
J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison Wesley, 1996.
S. P. Harbison. Modula-3. Prentice Hall, 1991.
R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In POPL’ 94 [37], pages 123–137.
R. Harper, J. C. Mitchell, and E. Moggi. Higher-order modules and the phase distinction. In Conf. Rec. 17th Ann. ACM Symp. Princ. of Prog. Langs., 1990.
R. Harper and B. Pierce. A record calculus based on symmetric concatenation. Technical Report CMU-CS-90-157R, Carnegie Mellon Univ., 2 July 1991.
M. P. Jones. From Hindley-Milner types to first-class structures. In Proceedings of the Haskell Workshop, La Jolla, California, U.S.A., 25 June 1995.
M. P. Jones. Using parameterized signatures to express modular structure. In Conf. Rec. POPL’ 96: 23rd ACM Symp. Princ. of Prog. Langs., 1996.
S. Krishnamurthi and M. Felleisen. Toward a formal theory of extensible software. In Sixth ACM SIGSOFT Symposium on the Foundations of Software Engineering, Nov. 1998.
X. Leroy. Manifest types, modules, and separate compilation. In POPL’ 94 [37], pages 109–122.
M. Lillibridge. Translucent Sums: A Foundation for Higher-Order Module Systems. PhD thesis, Carnegie Mellon Univ., May 1997.
E. Machkasova and F. Turbak. A calculus for link-time compilation. In Proc. European Symp. on Programming [2].
R. Milner, M. Tofte, R. Harper, and D. B. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1990.
Conf. Rec. 21st Ann. ACM Symp. Princ. of Prog. Langs., 1994.
Conf. Rec. POPL’ 99: 26th ACM Symp. Princ. of Prog. Langs., 1999.
D. Rémy. Projective ML. In Proc. 1992 ACM Conf. LISP Funct. Program., 1992.
J. G. Riecke and C. A. Stone. Privacy via subsumption. Theory and Practice of Object Systems, 199X. To appear.
C. V. Russo. Types for Modules. PhD thesis, Univ. of Edinburgh, 1998.
O. Waddell and R. K. Dybvig. Extending the scope of syntactic abstraction. In POPL’ 99 [38].
M. Wand. Type inference for record concatenation and multiple inheritance. In Proc. 4th Ann. Symp. Logic in Computer Sci., pages 92–97, Pacific Grove, CA, U.S.A., June 5–8 1989. IEEE Comput. Soc. Press.
J. B. Wells and R. Vestergaard. Confluent equational reasoning for linking with first-class primitive modules (long version). A short version is [45]. Full paper with three appendices for proofs, Aug. 1999.
J. B. Wells and R. Vestergaard. Equational reasoning for linking with first-class primitive modules. In Proc. European Symp. on Programming [2]. A long version is [44].
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wells, J.B., Vestergaard, R. (2000). Equational Reasoning for Linking with First-Class Primitive Modules. In: Smolka, G. (eds) Programming Languages and Systems. ESOP 2000. Lecture Notes in Computer Science, vol 1782. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46425-5_27
Download citation
DOI: https://doi.org/10.1007/3-540-46425-5_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67262-3
Online ISBN: 978-3-540-46425-9
eBook Packages: Springer Book Archive