A type system for higher-order modules

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A type system for higher-order modules

Full text

Pdf (174 KB)

Source

ACM SIGPLAN Notices archive
Volume 38 , Issue 1 (January 2003) table of contents

Pages: 236 - 249

Year of Publication: 2003

ISSN:0362-1340

Also published in ...

Authors

Derek Dreyer	Carnegie Mellon University, Pittsburgh, PA
Karl Crary	Carnegie Mellon University, Pittsburgh, PA
Robert Harper	Carnegie Mellon University, Pittsburgh, PA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 9, Downloads (12 Months): 49, Citation Count: 25

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/640128.604151 What is a DOI?

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

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked 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

CITED BY 25

	James J. Leifer , Gilles Peskine , Peter Sewell , Keith Wansbrough, Global abstraction-safe marshalling with hash types, ACM SIGPLAN Notices, v.38 n.9, p.87-98, September 2003
	Andreas Rossberg, Generativity and dynamic opacity for abstract types, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.241-252, August 27-29, 2003, Uppsala, Sweden
	Derek Dreyer, A type system for well-founded recursion, ACM SIGPLAN Notices, v.39 n.1, p.293-305, January 2004
	Eijiro Sumii , Benjamin C. Pierce, A bisimulation for dynamic sealing, ACM SIGPLAN Notices, v.39 n.1, p.161-172, January 2004
	Manuel M. T. Chakravarty , Gabriele Keller , Simon Peyton Jones , Simon Marlow, Associated types with class, ACM SIGPLAN Notices, v.40 n.1, p.1-13, January 2005
	Dimitrios Vytiniotis , Geoffrey Washburn , Stephanie Weirich, An open and shut typecase, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.13-24, January 10-10, 2005, Long Beach, California, USA
	Norman Ramsey , Kathleen Fisher , Paul Govereau, An expressive language of signatures, ACM SIGPLAN Notices, v.40 n.9, September 2005
	Derek Dreyer, Recursive type generativity, ACM SIGPLAN Notices, v.40 n.9, September 2005
	Manuel M. T. Chakravarty , Gabriele Keller , Simon Peyton Jones, Associated type synonyms, ACM SIGPLAN Notices, v.40 n.9, September 2005
	DEREK DREYER, Recursive type generativity, Journal of Functional Programming, v.17 n.4-5, p.433-471, July 2007
	Daniel K. Lee , Karl Crary , Robert Harper, Towards a mechanized metatheory of standard ML, ACM SIGPLAN Notices, v.42 n.1, January 2007
	Derek Dreyer , Robert Harper , Manuel M. T. Chakravarty , Gabriele Keller, Modular type classes, ACM SIGPLAN Notices, v.42 n.1, January 2007
	Martin Sulzmann , Manuel M. T. Chakravarty , Simon Peyton Jones , Kevin Donnelly, System F with type equality coercions, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France
	Karl Crary, Sound and complete elimination of singleton kinds, ACM Transactions on Computational Logic (TOCL), v.8 n.2, p.8-es, April 2007
	Eijiro Sumii , Benjamin C. Pierce, A bisimulation for dynamic sealing, Theoretical Computer Science, v.375 n.1-3, p.169-192, May, 2007
	Andreas Rossberg, The missing link: dynamic components for ML, ACM SIGPLAN Notices, v.41 n.9, September 2006
	Scott Owens , Matthew Flatt, From structures and functors to modules and units, ACM SIGPLAN Notices, v.41 n.9, September 2006
	John Billings , Peter Sewell , Mark Shinwell , Rok Strniša, Type-safe distributed programming for OCaml, Proceedings of the 2006 workshop on ML, September 16-16, 2006, Portland, Oregon, USA
	Oleg Kiselyov , Chung-chieh Shan, Lightweight Static Capabilities, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.7, p.79-104, June, 2007
	Derek Dreyer , Andreas Rossberg, Mixin' up the ML module system, ACM SIGPLAN Notices, v.43 n.9, September 2008
	Amal Ahmed , Derek Dreyer , Andreas Rossberg, State-dependent representation independence, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
	Benoît Montagu , Didier Rémy, Modeling abstract types in modules with open existential types, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
	Derek Dreyer, A type system for recursive modules, ACM SIGPLAN Notices, v.42 n.9, September 2007
	Andreas Rossberg, Dynamic Translucency with Abstraction Kinds and Higher-Order Coercions, Electronic Notes in Theoretical Computer Science (ENTCS), 218, p.313-336, October, 2008
	Kenneth Knowles , Cormac Flanagan, Compositional reasoning and decidable checking for dependent contract types, Proceedings of the 3rd workshop on Programming languages meets program verification, January 20-20, 2009, Savannah, GA, USA