Semantic typing for parametric algebraic specifications

The implementation relation of refinement of specifications is studied in the framework of the calculus of higher-order parameterization of specifications. An existing system of derivation of the relation among non-parametric specifications is enlarged so as to comprise parametric specifications. The new system is correct and complete under certain assumptions. By means of this system the calculus of parametric specifications can be enhanced with semantic types, and in this way a specification is a valid argument of a parametric specification as long as it shows the particular behavior demanded by the semantic parameter restriction. This typing can be derived, and so function application is conditional to the derivability of the parameter restrictions instantiated with the actual argument.