Using Parameterized Signatures to Express Modular Structure

12 years 1 months ago
Using Parameterized Signatures to Express Modular Structure
Module systems are a powerful, practical tool for managing the complexity of large software systems. Previous attempts to formulate a type-theoretic foundation for modular programming have been based on existential, dependent, or manifest types. These approaches can be distinguished by their use of different quantifiers to package the operations that a module exports together with appropriate implementation types. In each case, the underlying type theory is simple and elegant, but significant and sometimes complex extensions are needed to account for features that are important in practical systems, such as separate compilation and propagation of type information between modules. This paper presents a simple type-theoretic framework for modular programming using parameterized signatures. The use of quantifiers is treated as a necessary, but independent concern. Using familiar concepts of polymorphism, the resulting module system is easy to understand and admits true separate compilati...
Mark P. Jones
Added 08 Aug 2010
Updated 08 Aug 2010
Type Conference
Year 1996
Where POPL
Authors Mark P. Jones
Comments (0)