General Terms Languages, Theory

Abstract We present a type theory for higher-order modules that accountsfor 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 providea complete and practical formalization of all of these critical issues in module system design