Extra Theory Morphisms forInstitutions (abstract)
We extend the ordinary concept of theory morphism in institutions
to extra theory morphisms. Extra theory morphisms map theories belonging
to different institutions across institution morphisms. We investigate
the basic mathematical properties of extra theory morphisms supporting
the semantics of logical multi-paradigm languages, especially module systems
a la OBJ-Clear. They include model reducts, free constructions (liberality),
co-limits, and model amalgamation (exactness).
We outline a general logical semantics for languages whose semantics
satisfy certain ``logical'' principles by extending the institutional semantics
developed within the Clear-OBJ tradition. Finally, in the Appendix, we
briefly illustrate it with the concrete example of CafeOBJ.
full paper--183K.
Back to CafeOBJ Home Page