An lgebraic framework for higher-order odules
Rosa Jiménez6 and Fernando Orejas6
| (6) |
Dept. Leng. Sist. Inf., Univ. Polit. Catalunya, Barcelona, SPAIN |
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 pri- ori 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.
Acknowledgements This work initially started in cooperation with Hartmut Ehrig. Although he gave it up after some time, afterwards we still
had some useful discussions. This work has been partially supported by Spanish CICYT projects COSMOS (ref. TIC95-1016-C02-01)
and HEMOSS (ref. TIC98-0949-C02-01).
References secured to subscribers.