Abstract

We give a semantics of parameterised modules in the framework of functorial semantics. We first introduce two mathematical tools. One is the notion of "Cartesian closed sketch," which enables a functorial semantics of simply typed lambda calculi. Another tool is the Power and Robinson's recent formulation of the notion of observational equivalence in a simply typed lambda calculus context. We then apply these tools to give a semantics of parameterised modules. We also give an account of what it means for a module to be correct up to observational equivalence. We wish to claim that our functorial method makes it easier to put the emphasis on the essential structure than the traditional universal algebraic approach does, and it is that conceptual simplicity that enabled us to obtain a straightforward proof of some theorems considered to be hard or to extend some traditional notions naturally. This is joint work with Don Sannella.