Extra Theory Morphisms for Institutions (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.

back to Selected Publications