- Institution (computer science)
The notion of

**institution**has been created byJoseph Goguen andRod Burstall in the late 1970'sin order to deal with the "population explosion among thelogical system s used incomputer science ". The notion tries to capture the essence of the concept of "logical system".With this, it is possible to develop concepts ofspecification language s (like structuring of specifications, parameterization, implementation, refinement, development),proof calculi and eventool s in a way completely independent of the underlying logical system. There are also morphisms that allow to relate and translate logical systems. Important applications of this are re-use of logical structure (also called borrowing), heterogeneous specification and combination of logics. Recently,institutional model theory has generalized many notions and deep results ofmodel theory .**Definition**The theory of institutions does not assume anything about the nature of the logical system. That is, models and sentences may be arbitrary objects; the only assumption being that there is a

**satisfaction relation**between models and sentences, telling whether a sentence holds in a model or not. Satisfaction is inspired by Tarski's truth definition, but can in fact be any binary relation.A crucial feature of institutions now is that models, sentences and their satisfaction are always being considered to live in some vocabulary or context (called**signature**) that defines the (non-logical) symbols that may be used in sentences and that need to be interpreted in models. Moreover,**signature morphisms**allow to extend signatures, change notation etc. Nothing is assumed about signatures and signature morphisms except that signature morphisms can be composed; this amounts to having a

category of signatures and morphisms. Finally, it is assumed that signature morphisms lead to translations of sentences and models in a way that satisfaction is preserved. While sentences are translated along with signature morphisms (think of symbols being replaced along the morphism), models are translated (or better: reduced)**against**signature morphisms: for example, in case of a signature extension, a model of the (larger) target signature may be reduced to a model of the (smaller) source signature by just forgetting some components of the model.Formally, an institution consists of

* a category $Sign$ of

**signatures**,

* afunctor $sen:Sign\; o$Set giving, for each signature $Sigma$, the set of**sentences**$sen(Sigma)$, and for each signature morphism $sigma:Sigma\; oSigma\text{'}$, the**sentence translation map**$sen(sigma):sen(Sigma)\; o\; sen(Sigma\text{'})$, where often $sen(sigma)(varphi)$ is written as $sigma(varphi)$,

* afunctor $Mod:Sign^\{op\}\; o$Cat giving, for each signature $Sigma$, the category of**models**$Mod(Sigma)$, and for each signature morphism $sigma:Sigma\; oSigma\text{'}$, the**reduct functor**$Mod(sigma):Mod(Sigma\text{'})\; o\; Mod(Sigma)$, where often $Mod(sigma)(M\text{'})$ is written as $M\text{'}|\_\{sigma\}$,

* a satisfaction relation $\{models\_\{Sigmasubseteq|\{Mod(Sigma)|\; imes\; sen(Sigma)\}$ for each $Sigmain\; Sign$,such that for each $sigma:Sigma\; oSigma\text{'}$ in $Sign$ the following

**satisfaction condition**holds:$M\text{'}models\_\{Sigma\text{'}\}sigma(varphi)$ if and only if $M\text{'}|\_\{sigma\}models\_\{Sigma\}\; varphi$

for each $M\text{'}in\; Mod(Sigma\text{'})$ and $varphiin\; sen(Sigma)$.

The satisfaction condition expresses that truth is invariant under change of notation (and also under enlargement or quotienting of context).

Strictly speaking, the model functor ends in the

quasi-category of all large categories.**Examples of Institutions***

First-order logic

*Higher-order logic

*Intuitionistic logic

*Modal logic

*Temporal logic

* CASL**Papers*** J. A. Goguen and R. M. Burstall, Introducing Institutions, Lecture Notes in Computer Science 164, pp. 221-256, 1984.

* J. A. Goguen and R. M. Burstall, Institutions: Abstract Model Theory for Specification and Programming, Journal of the Association for Computing Machinery 39, pp. 95-146, 1992.

* J. Meseguer, General Logics, Logic Colloquium 87, pp. 275-329, North Holland, 1989.

* J. A. Goguen and G. Rosu, Institution morphisms, Formal aspects of computing 13, pp. 274-307, 2002.

* D. Sannella and A. Tarlecki, Specifications in an arbitrary institution, Information and Computation 76, pp. 165-210, 1988

* T. Mossakowski, J. A. Goguen, R. Diaconescu, A. Tarlecki. What is a Logic?. In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113–133. Birkhäuser 2005.**External links*** [

*http://www-cse.ucsd.edu/users/goguen/projs/inst.html Institutions by Joseph Goguen*]

* [*http://www.informatik.uni-bremen.de/flirts/ Formalism, Logic, Institution - Relating, Translating and Structuring*] (including large bibliography)

* [*http://www.imar.ro/~diacon/publications.html#Institutions__institution-independent Razvan Diaconescu's publication list*] - contains recent work on institutional model theory**ee also***

Entailment system

*Abstract model theory

*Wikimedia Foundation.
2010.*

### Look at other dictionaries:

**Computer science**— or computing science (abbreviated CS) is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems. Computer scientists invent algorithmic… … Wikipedia**Tudor Vianu National College of Computer Science**— Coordinates: 44°27′29″N 26°04′47″E / 44.45806°N 26.07972°E / 44.45806; 26.07972 … Wikipedia**Logic in computer science**— describes topics where logic is applied to computer science and artificial intelligence. These include:*Investigations into logic that are guided by applications in computer science. For example: Combinatory logic and Abstract interpretation;… … Wikipedia**Swedish Institute of Computer Science**— The Swedish Institute of Computer Science, SICS, is an independent non profit research organization with a research focus on applied computer science. The institute carries out research in a number of areas, including networked embedded systems,… … Wikipedia**Grigore Moisil National College of Computer Science (Braşov)**— Grigore Moisil National College of Computer Science Established 1938 Type Highschool Headmaster Mariana Bulbuc Students 672 Grades … Wikipedia**National Institute for Research in Computer Science and Control**— The National Institute for Research in Computer Science and Control (French: Institut national de recherche en informatique et en automatique, INRIA) is a French national research institution focusing on computer science, control theory and… … Wikipedia**Department of Computer Science (University of Copenhagen)**— DIKU Department of Computer Science, University of Copenhagen (Danish: Datalogisk Institut, Københavns Universitet), commonly referred to by its acronym DIKU, is an institute of research and education in computer science at the Faculty of Science … Wikipedia**Master of Computer Science**— Der Master ([ˈmaːstɐ] oder [ˈmaːstə], aus engl. master, das auf lat. magister „Lehrer“, „Vorsteher“, „Meister“ zurückgeht) ist in vielen europäischen Staaten der zweite akademische Grad, den Studenten an Hochschulen als Abschluss einer… … Deutsch Wikipedia**Doctor of Computer Science**— The degree of Doctor of Computer Science (DCompSci, DSc.Comp, D.C.S.) is an applied research doctorate. The DCompSci often requires coursework beyond the masters level in addition to research that results in a dissertation that contributes to… … Wikipedia**Institution**— Sociology … Wikipedia