Theory of coalgebras

Coalgebras are simple mathematical structures for describing dynamical systems (like automata, transition systems, classes in object-oriented languages, processes) in a very general way. A coalgebra consists of a set X, often called the state space, together with certain operations for observation and modification. These operations are combined in a single function of the form X --> T(X), where T(X) is a type or functor representing the interface of the system. Examples of coalgebras are:

• Deterministic automata, say over an alphabet A. They can be described as a function c = (next, final) : X --> (A => X) x {0,1}. The function next : X --> (A => X) tells for a state x in X and a symbol a in A what the successor state next(x)(a) in X is. And the function final : X --> {0,1} tells whether a state is final or not.
• Transition systems, say with labels L. They can be described as coalgebras with the powerset P in its interface type: a function c : X --> P(L x X) captures the system where c(x) = {(l,y) | x can do an l-step to y}.
• Classes, as models of class specifications, like in the QUEUE. The associated QUEUE interface type is

  T(X) = int x (A => X) x (1 + (A x X))

  and coalgebras X --> T(X) combine an interpretation of the three methods size, push, pop of this class in a single function. Notice that at this stage we only describe a model of the interface, ignoring the assertions. Taking these into account means that one restricts oneself to those coalgebras X --> T(X) that satisfy the QUEUE assertions.
• Java classes, with the interface type of the associated coalgebra given by the cartesian product of the types of the fiels and of the methods of the class.

The advantage of a description in terms of coalgebras is that it enables application of standard notions and techniques from the theory of coalgebras like invariant, bisimulation, behaviour (via final coalgebras), refinement, coinduction (as proof principle involving final coalgebras), temporal logic (with henceforth and eventually operators).

The main forum for work on coalgebra is the workshop Coalgebraic Methods in Computer Science (CMCS), which is usually held as satellite event to ETAPS.
There is also a more general forum on behavioral aspects of computer science and mathematics, maintained at UCSD.