zbMATH — the first resource for mathematics

An algebraic framework for higher-order modules. (English) Zbl 0953.68097
Wing, Jeannette M. (ed.) et al., FM ’99. Formal methods. World congress on Formal methods in the development of computing systems. Toulouse, France, September 20–24, 1999. Proceedings. In 2 vols. Berlin: Springer (ISBN 3-540-66587-0/vol1; 3-540-66588-9/vol2). Lect. Notes Comput. Sci. 1708; 1709, 1778-1797 (1999).
Summary: 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 \(\lambda\)-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 \(\lambda\)-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 \(\beta\)-reduction with respect to the semantics given.
For the entire collection see [Zbl 0929.00076].

68Q65 Abstract data types; algebraic specification
03B40 Combinatory logic and lambda calculus
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
18C50 Categorical semantics of formal languages
PDF BibTeX Cite