Grothendieck Institutions (abstract)
 We extend indexed categories, fibred categories, and Grothendieck
constructions to institutions. We show that the 2category of
institutions admits Grothendieck constructions (in a general
2categorical sense) and that any split fibred institution is
equivalent to a Grothendieck institution of an indexed institution.
 We use Grothendieck institutions as the underlying mathematical
structure for the semantics of multiparadigm (heterogenous)
algebraic specification. We recuperate the socalled `extra theory
morphisms' as ordinary theory morphisms in a Grothendieck
institution. We investigate the basic mathematical properties of
Grothendieck institutions, such as theory colimits, liberality (free
constructions), exactness (model amalgamation), and inclusion
systems by `globalisation' from the `local' level of the indexed
institution to the level of the Grothendieck institution.

back to Selected Publications