Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

We present a type theory for higher-order modules that accounts for many central issues in module system design, including translucency, applicativity, generativity, and modules as first-class values. Our type system harmonizes design elements from previous work, resulting in a simple, economical account of modular programming. The main unifying principle is the treatment of abstraction mechanisms as computational effects. Our language is the first to provide a complete and practical formalization of all of these critical issues in module system design.

REFERENCES

• 1: David R. Aspinall. Type Systems for Modular Programs and Specifications. PhD thesis, Edinburgh University, Edinburgh, Scotland, December 1997.
• 2: L. Cardelli , J. Donahue , M. Jordan , B. Kalsow , G. Nelson, The Modula–3 type system, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.202-212, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75295]
• 3: Luca Cardelli and Xavier Leroy. Abstract types and the dot notation. In M. Broy and C. B. Jones, editors, Proceedings IFIP TC2 working conference on programming concepts and methods, pages 479--504. North-Holland, 1990. Also available as research report 56, DEC Systems Research Center.
• 4: Karl Crary, Sound and Complete Elimination of Singleton Kinds, Selected papers from the Third International Workshop on Types in Compilation, p.1-26, September 21, 2000
• 5: Karl Crary , Robert Harper , Sidd Puri, What is a recursive module?, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.50-63, May 01-04, 1999, Atlanta, Georgia, United States
• 6: Derek Dreyer. Moscow ML's higher-order modules are unsound. Posted to the TYPES electronic forum, September 2002.
• 7: Derek Dreyer, Karl Crary, and Robert Harper. A type system for higher-order modules (expanded version). Technical Report CMU-CS-02-122R, School of Computer Science, Carnegie Mellon University, December 2002.
• 8: Matthew Flatt , Matthias Felleisen, Units: cool modules for HOT languages, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.236-248, June 17-19, 1998, Montreal, Quebec, Canada
• 9: Giorgio Ghelli , Benjamin Pierce, Bounded existentials and minimal typing, Theoretical Computer Science, v.193 n.1-2, p.75-96, Feb. 28, 1998 [doi>10.1016/S0304-3975(96)00300-3]
• 10: Warren D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225--230, 1981.
• 11: Robert Harper , Mark Lillibridge, A type-theoretic approach to higher-order modules with sharing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.123-137, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176927]
• 12: Robert Harper , John C. Mitchell , Eugenio Moggi, Higher-order modules and the phase distinction, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.341-354, December 1989, San Francisco, California, United States [doi>10.1145/96709.96744]
• 13: Robert Harper , Christopher Stone, A type-theoretic interpretation of standard ML, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
• 14: Xavier Leroy, Manifest types, modules, and separate compilation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.109-122, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176926]
• 15: Xavier Leroy, Applicative functors and fully transparent higher-order modules, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.142-153, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199476]
• 16: Xavier Leroy. A syntactic theory of type generativity and sharing. Journal of Functional Programming, 6(5):667--698, 1996.
• 17: Xavier Leroy, A modular module system, Journal of Functional Programming, v.10 n.3, p.269-303, May 2000 [doi>10.1017/S0956796800003683]
• 18: Mark Lillibridge. Translucent Sums: A Foundation for Higher-Order Module Systems. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, December 1996.
• 19: Barbara Liskov , John Guttag, Abstraction and specification in program development, MIT Press, Cambridge, MA, 1986
• 20: David B. MacQueen, Using dependent types to express modular structure, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.277-286, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512670]
• 21: David B. MacQueen , Mads Tofte, A Semantics for Higher-Order Functors, Proceedings of the 5th European Symposium on Programming: Programming Languages and Systems, p.409-423, April 11-13, 1994
• 22: Robin Milner , Mads Tofte , Robert Harper, The Definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 23: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 24: John Mitchell , Sigurd Meldal , Neel Madhav, An extension of standard ML modules with subtyping and inheritance, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.270-278, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99620]
• 25: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• 26: Moscow ML. http://www.dina.dk/~sestoft/mosml.html+.
• 27: Objective Caml. http://www.ocaml.org+.
• 28: Claudio V. Russo. Types for Modules. PhD thesis, Edinburgh University, Edinburgh, Scotland, 1998. LFCS Thesis ECS--LFCS--98--389.
• 29: Claudio V. Russo, First-class structures for standard ML, Nordic Journal of Computing, v.7 n.4, p.348-374, Winter 2000
• 30: Claudio V. Russo, Recursive structures for standard ML, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
• 31: Zhong Shao, Transparent modules with fully syntatic signatures, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.220-232, September 27-29, 1999, Paris, France
• 32: Christopher Allan Stone , Robert Harper, Singleton kinds and singleton types, 2000
• 33: Christopher A. Stone , Robert Harper, Deciding type equivalence in a language with singleton kinds, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325724]
• 34: N. Wirth, Programming in Modula-2, Springer-Verlag Telos, 1983

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types; Modules, packages

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Theory

Keywords:
abstract data types, computational effects, functors, generativity, modularity, singleton types, type theory