A Category-theoretic Account of Program Modules

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.

• Type: Conference
• Year: 1989
• Where: CTCS
• Authors: Eugenio Moggi
• Keywords: CTCS 1989, Indexed Categories, Programming Languages, Type-theoretic Explanation