An algebraic framework for higher-order modules

Abstract

This paper presents a new framework for dealing with higher- order parameterization allowing the use of arbitrary fitting morphisms for parameter passing. In particular, we define a category of higher-order parameterized or module specifications and, then, following the approach started in the ASL specification language, we define a typed λ-calculus, as a formalism for dealing with these specifications, where arbitrary fitting morphisms are allowed. In addition, the approach presented is quite general since all the work is independent of the kind of basic specifications considered and, also, of the kind of operations used for building basic specifications, provided that some conditions hold. In this sense we are not especially bound to any set of basic specification-building operations. We call our parameterized units modules to make clear the distinction between the basic specification level that is not fixed a priori and the parameterized units level that is studied in the paper. The kind of calculus presented can be seen as a variation/extension of the simply typed λ-calculus, which means that we do not allow dependent types. This would have been interesting, but it is not possible with the semantics proposed. The main result of the paper shows the adequacy of,β-reduction with respect to the semantics given.