Equational Reasoning for Linking with First-Class Primitive Modules

  • J. B. Wells
  • René Vestergaard
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1782)


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.


Module System Output Component Contraction Relation Lambda Calculus Input Component 
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.


  1. [1]
    Haskell 98: A non-strict, purely functional language. Technical report, The Haskell 98 Committee, 1 Feb. 1999. Currently available at
  2. [2]
    LNCS. Springer-Verlag, 2000.Google Scholar
  3. [3]
    M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag, 1996.Google Scholar
  4. [4]
    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.Google Scholar
  5. [5]
    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.Google Scholar
  6. [6]
    Z. M. Ariola and S. Blom. Cyclic lambda calculi. In Theoretical Aspects Comput. Softw.: Int’l Conf., 1997.Google Scholar
  7. [7]
    Z. M. Ariola and S. Blom. Lambda calculi plus letrec. Submitted, 3 July 1997.Google Scholar
  8. [8]
    Z. M. Ariola and J. W. Klop. Lambda calculus with explicit recursion. Inf. & Comput., 139:154–233, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  9. [9]
    H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, revised edition, 1984.Google Scholar
  10. [10]
    J. G. P. Barnes. Programming in Ada 95. Addison-Wesley, 1996.Google Scholar
  11. [11]
    V. Bono, M. Bugliesi, M. Dezani-Ciancaglini, and L. Liquori. Subtyping constraints for incomplete objects. Fundamenta Informaticae, 199X. To appear.Google Scholar
  12. [12]
    G. Bracha. The Programming Language Jigsaw: Mixins, Modularity, and Multiple Inheritance. PhD thesis, Univ. of Utah, Mar. 1992.Google Scholar
  13. [13]
    G. Bracha and G. Lindstrom. Modularity meets inheritance. In Proc. Int’l Conf. Computer Languages, pages 282–290, 1992.Google Scholar
  14. [14]
    L. Cardelli. Program fragments, linking, and modularization. In Conf. Rec. POPL’ 97: 24th ACM Symp. Princ. of Prog. Langs., 1997.Google Scholar
  15. [15]
    K. Crary, R. Harper, and S. Puri. What is a recursive module? In Proc. ACM SIGPLAN’ 99 Conf. Prog. Lang. Design & Impl., 1997.Google Scholar
  16. [16]
    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.Google Scholar
  17. [17]
    D. Duggan and C. Sourelis. Mixin modules. In Proc. 1996 Int’l Conf. Functional Programming, pages 262–273, 1996.Google Scholar
  18. [18]
    D. Duggan and C. Sourelis. Parameterized modules, recursive modules, and mixin modules. In ACM SIGPLAN Workshop on ML and its Applications, 1998.Google Scholar
  19. [19]
    R. B. Findler and M. Flatt. Modular object-oriented programming with units and mixins. In Proc. 1998 Int’l Conf. Functional Programming, 1998.Google Scholar
  20. [20]
    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.zbMATHMathSciNetGoogle Scholar
  21. [21]
    M. Flatt and M. Felleisen. Units: Cool modules for HOT languages. In Proc. ACM SIGPLAN’ 98 Conf. Prog. Lang. Design & Impl., 1998.Google Scholar
  22. [22]
    M. Flatt, S. Krishnamurthi, and M. Felleisen. Classes and mixins. In Conf. Rec. POPL’ 98: 25th ACM Symp. Princ. of Prog. Langs., 1998.Google Scholar
  23. [23]
    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.Google Scholar
  24. [24]
    N. Glew and G. Morrisett. Type-safe linking and modular assembly language. In POPL’ 99 [38].Google Scholar
  25. [25]
    J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison Wesley, 1996.Google Scholar
  26. [26]
    S. P. Harbison. Modula-3. Prentice Hall, 1991.Google Scholar
  27. [27]
    R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In POPL’ 94 [37], pages 123–137.Google Scholar
  28. [28]
    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.Google Scholar
  29. [29]
    R. Harper and B. Pierce. A record calculus based on symmetric concatenation. Technical Report CMU-CS-90-157R, Carnegie Mellon Univ., 2 July 1991.Google Scholar
  30. [30]
    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.Google Scholar
  31. [31]
    M. P. Jones. Using parameterized signatures to express modular structure. In Conf. Rec. POPL’ 96: 23rd ACM Symp. Princ. of Prog. Langs., 1996.Google Scholar
  32. [32]
    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.Google Scholar
  33. [33]
    X. Leroy. Manifest types, modules, and separate compilation. In POPL’ 94 [37], pages 109–122.Google Scholar
  34. [34]
    M. Lillibridge. Translucent Sums: A Foundation for Higher-Order Module Systems. PhD thesis, Carnegie Mellon Univ., May 1997.Google Scholar
  35. [35]
    E. Machkasova and F. Turbak. A calculus for link-time compilation. In Proc. European Symp. on Programming [2].Google Scholar
  36. [36]
    R. Milner, M. Tofte, R. Harper, and D. B. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1990.Google Scholar
  37. [37]
    Conf. Rec. 21st Ann. ACM Symp. Princ. of Prog. Langs., 1994.Google Scholar
  38. [38]
    Conf. Rec. POPL’ 99: 26th ACM Symp. Princ. of Prog. Langs., 1999.Google Scholar
  39. [39]
    D. Rémy. Projective ML. In Proc. 1992 ACM Conf. LISP Funct. Program., 1992.Google Scholar
  40. [40]
    J. G. Riecke and C. A. Stone. Privacy via subsumption. Theory and Practice of Object Systems, 199X. To appear.Google Scholar
  41. [41]
    C. V. Russo. Types for Modules. PhD thesis, Univ. of Edinburgh, 1998.Google Scholar
  42. [42]
    O. Waddell and R. K. Dybvig. Extending the scope of syntactic abstraction. In POPL’ 99 [38].Google Scholar
  43. [43]
    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.Google Scholar
  44. [44]
    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.Google Scholar
  45. [45]
    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].Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • J. B. Wells
    • 1
  • René Vestergaard
    • 1
  1. 1.Heriot-Watt UniversityUK

Personalised recommendations