A category-theoretic account of program modules
- 4 March 1991
- journal article
- research article
- Published by Cambridge University Press (CUP) in Mathematical Structures in Computer Science
- Vol. 1 (1) , 103-139
- https://doi.org/10.1017/s0960129500000074
Abstract
The type-theoretic explanation of modules proposed to date (for programming languages like ML) is unsatisfactory, because it does not capture that the evaluation of type-expressions is independent from the evaluation of program expressions. We propose a new explanation based on ‘programming languages as indexed categories’ and illustrate 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 also outlines a methodology, which may lead to a modular approach in the study of programming languages.Keywords
This publication has 15 references indexed in Scilit:
- Higher-order modules and the phase distinctionPublished by Association for Computing Machinery (ACM) ,1990
- Alpha-conversion, conditions on variables and categorical logicStudia Logica, 1989
- Categorical semantics for higher order polymorphic lambda calculusThe Journal of Symbolic Logic, 1987
- Fibered categories and the foundations of naive category theoryThe Journal of Symbolic Logic, 1985
- Modules for standard MLPublished by Association for Computing Machinery (ACM) ,1984
- Locally cartesian closed categories and type theoryMathematical Proceedings of the Cambridge Philosophical Society, 1984
- HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITIONMathematical Logic Quarterly, 1983
- Abstract families and the adjoint functor theoremsPublished by Springer Nature ,1978
- Fibrations and Yoneda's lemma in a 2-categoryPublished by Springer Nature ,1974
- The formal theory of monadsJournal of Pure and Applied Algebra, 1972