Abstract:
The programming language Standard ML is an amalgam of two, largely orthogonal, languages. The Core language expresses details of algorithms and data structures. The Modules language expresses the modular architecture of a software system. Both languages are statically typed, with their static and dynamic semantics specified by a formal definition.
Over the past decade, Standard ML Modules has been the source of inspiration for much research into the type-theoretic foundations of modules languages. Inspired by the syntax of Modules, these efforts have resulted in new theories based on dependent types, without giving a type-theoretic account of the original static semantics. In this talk, I use Type Theory to recast the unconventional static semantics of Modules in more familiar terms.
I will present an equivalent, but more type-theoretic, reformulation of the static semantics of Modules. This presentation makes clear that the concepts underlying Modules are type parameterisation, type quantification and subtyping. In contrast to recent work on modules, this type theory avoids the use of first-order dependent types. The theory also supports natural generalisations to higher-order and first-class modules.
Presented at 1999 Workshop on Dependent Types in Programming, Gothenburg, Sweden, March 1999.
This is a set of 21 slides. It is available in the following formats: