Extra theory morphisms for institutions: Logical semantics for multi-paradigm languages. (English) Zbl 0919.68087

Summary: We extend the ordinary concept of theory morphisms 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 structuring specifications (module systems) à la OBJ-Clear. They include model reducts, free constructions (liberality), co-limits, model amalgamation (exactness), and inclusion systems.
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 this with the concrete example of CafeOBJ.


68Q55 Semantics in the theory of computing
68Q45 Formal languages and automata
18C10 Theories (e.g., algebraic theories), structure, and semantics
03G30 Categorical logic, topoi
08A70 Applications of universal algebra in computer science


Full Text: DOI