Footnotes

 

(1)

Though this condition is not computable and hence cannot be enforced by the tools, it seems worth to have it in the semantics, otherwise it would be better to have a construct extracting the signature from a specification and use it to describe the typing of parameters to stress that the semantics of the typing does not carry any mening.  

(2)

rules to disambiguate overloaded generic symbols will be the same assumed otherwise in the language for signature morphisms