A type system for higher-order modules

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 t 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.

• Type: Conference
• Year: 2003
• Where: POPL
• Authors: Derek Dreyer, Karl Crary, Robert Harper
• Keywords: Economical Account, First-class Values, Main Unifying Principle, POPL 2003, Programming Languages