Unified algebras and institutions

A framework for algebraic specification of abstract data types is introduced. It involves so-called unified algebras, where sorts are treated as values, so that operations can be applied to sorts as well as to the elements that they classify. An institution for unified algebras is defined and shown to be liberal. However, the ordinary forgetful functor does not forget any values in unified algebras, so the usual data constraints do not have any models. A more forgetful functor is introduced and used to define so-called bounded data constraints, which have the expected models