Dialgebraic Logics

EPSRC-funded Visiting Fellowship GR/M36694
for Professor Horst Reichel, Technische Universität Dresden
1st September - 31st December 1998

Principle investigators: D T Sannella and G D Plotkin

The situation in the theories of concurrency and reactive systems is characterized by a multitude of formal models where none of them is clearly better than all the others overall with respect to applicability and formal foundations. In this situation research should focus on the most elementary process building operations on one hand and on formal approaches that allow each user to specify his or her own problem-oriented process type on the other. The research grant supported an activity of the second kind.

The outcome of the research grant is a category theoretic model theory that supports a uniform axiomatic specification of data types by means of the properties of the defining constructors and of process types by means of the properties of the observations (or experiments). The formal framework makes available inductive and co-inductive definitions and proof principles that can be implemented in interactive proof editors in future work.

The results of the research grant can serve as a starting point for an extension of the specification language CASL aimed at the axiomatic specification of reactive systems, one of the tasks of the ESPRIT-funded CoFI Working Group.


Don Sannella. Please mail me if you have any comments on this page.
Last modified: Tue Jun 29 12:03:49 BST 2004