|
Abstract : |
The type-theoretic explanation of modules proposed to date (for programming languages like ML) is unsatisfactory, because it does not capture that evaluation of type-expressions is independent from evaluation of programexpressions. We propose a new explanation based on \programming languages as indexed categories " and illustrates how ML can be extended to support higher order modules, by developing a category-theoretic semantics for a calculus of modules with dependent types. The paper outlines also a methodology, which may lead to a modular approach in the study of programming languages., |
