Coalgebras, Modal Logic, Stone Duality


EPSRC First Grant Scheme EP/C014014/1, GPB 118,516


August 2005 to July 2007.


Transition systems pervade much of computer science. This projects aims at a general theory of specification languages for transition systems. More specifically, transition systems will be generalised to coalgebras as in (Rutten, 2000). Specification languages together with their proof systems, in the following called (logical or modal) calculi, will be presented by the associated classes of algebras (eg propositional logic by Boolean algebras or intuitionistic logic by Heyting algebras). Stone duality (Johnstone, 1982) will be used to give a coalgebraic semantics for the logics represented by algebras. Stone duality has been used in the ground breaking work of (Jonnson and Tarski, 1951) and (Goldblatt, 1976) in modal logic and (Abramsky, 1991) in computer science. The coalgebraic approach to systems allows us to formalise the notion of a type of systems as a functor F. The generality of coalgebras resides in the possibility to build into F many different features like input, output, choice, nondeterminism, probability distributions, etc. The aim of this proposal is to develop the theory of logics for coalgebras not separately for each of these features but parametrically in F. This involves the following issues.

  1. Associate to any type F (possibly satisfying some mild conditions to be determined) a corresponding modal logic such that the logic is sound and complete and the semantics fully abstract. 
  2. Use the parametricity in the type F to describe modularity principles allowing to build complex proof systems from simpler ones. Show how this modularity is useful for the specification and verification of systems. 
  3. Develop a coalgebraic model theory of modal logic that is parametric in F. 
  4. Applying the general theory (which will be developed for the items above), it will typically be the case that one wants to relate a set-based semantics to a logic that has a topology-based Stone dual.
    Thus, the relationship of topologically-based structures and set-based structures will have to be investigated.


 A Kurz

Share this page:

Contact Us

Admissions Enquiries:
BSc: +44 (0) 116 252 5280
MSc: +44 (0) 116 252 2265
E: BSc
E: MSc

Departmental Enquiries:
T: +44 (0) 116 252 2129/3887
F: +44 (0) 116 252 3604

Dept of Informatics
University of Leicester
Leicester, LE1 7RH
United Kingdom


DisabledGo logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has a detailed accessibility guide for the Informatics Building.