|   | CMU-CS-02-122R Computer Science Department
 School of Computer Science, Carnegie Mellon University
 
    
     
 CMU-CS-02-122R
 
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.
 
CMU-CS-02-122R.psCMU-CS-02-122R.pdf
 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 
 |