We give a semantics of parameterised modules in higher order programming using the framework of functorial semantics. To that end, two mathematical tools are introduced. One is the Cartesian closed sketch, which is an instance of the general theory of sketches introduced by Kinoshita, Power and Takeyama. Sketches make it easier to develop a functorial semantics. Another is a formulation of observational equivalence in the setting of Cartesian closed categories, which is a mild modification of Power and Robinson's recent work. We then apply these tools to give a semantics of parameterised modules in typed lambda calculus. Our main result is the stability theorem of parameterised modules which says that, whenever two modules are observationally equivalent, applying an "observationally faithful" parameterised module to them yields equivalent results. Moreover, we show that whenever two parameterised modules are equivalent, applying them to a module yields an equivalent result. An advantage of our semantics, compared with semantics previously proposed, is that our formulation is closer to intuition, yet retains structural clarity.
Further research topics in this functorial approach to specification semantics would be to formulate the sharing of modules and the distinction between Sigma-algebras and (Sigma,AX)-algebras. In the usual universal algebraic approach, those algebraic structures without any axiomatic constraints (Sigma-algebras) play an important special role, but it is currently not obvious how to distinguish those structures from others in our functorial approach using sketches.