Computer Science Department
School of Computer Science, Carnegie Mellon University


A Type System for Higher-Order Modules
(Expanded Version)

Derek Dreyer, Karl Crary, Robert Harper

December 2002

This reports refines and supersedes the original version published in July 2002 as
Computer Science Technical Report CMU-CS-02-122.

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

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.

57 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by