Details of Grant 

EPSRC Reference:	EP/C014014/1
Title:	Coalgebras, Modal Logic, Stone Duality
Principal Investigator:	Kurz, Professor A
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science
Organisation:	University of Leicester
Scheme:	First Grant Scheme Pre-FEC
Starts:	01 February 2006	Ends:	31 May 2008	Value (£):	118,516
EPSRC Research Topic Classifications:	Fundamentals of Computing Logic & Combinatorics
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:
Summary on Grant Application Form
I.One of the central problems of programming computers is that it isvery difficult to write correct programs or to convince yourself ofthe correctness of some program. One way to tackle this problem is theuse of logic.Let us first take a brief look at logic. We can use logic to (1) make statements about the world, (2) define when a statement holds or does not hold in the world, (3) deduce new statements from given ones using rules of reasoning.`World' can mean the world we live in and logic was originally indeeddeveloped to reason about everyday problems. In mathematics, the worldone reasons about is the world of mathematical objects. Themathematical world is rich enough to model different notions ofcomputation. Mathematical logic thus allows us to devise differentlogics for different models of computation. The logics relevant forthis proposal are known as modal logics.The upshot of this effort should be to make reasoning aboutcomputations completely precise and thus to eliminate the errorshumans tend to make when reasoning about programs.II.In my project I will look at particular models of computation whichare called transition systems. Transition systems consist of statesand relations between states. The idea is that each state representsa given moment of the computation and the relations describe how thecomputation proceeds from on state to another.The project aims at a general theory of logics for transitionsystems. It will establish the relationship between logics andtransition systems via the following detour that allows us to use acertain mathematical theory known as Stone duality. Recent developments suggest using co-algebras to represent transitionsystems. Coalgebras are in a special relationship---calledduality---to algebras. In a similar way as known from solvingequations in school, algebra can be used to formulate reasoningprinciples.In particular, the aims of this proposal are the following. Toassociate to any type of transition system an appropriate logic. Toshow how these logics can be applied to the verification of statementsabout programs. To investigate how certain concepts and tools ofmathematical logic can be adapted to coalgebras and their logics.III.The project will contribute to the theory of coalgebras as a generaltheory of transition systems as developed in the 1990s by manyresearchers. It will also be an important contribution to the recentworks on the connections between (modal) logic andcoalgebras. Coalgebras and modal logic have received attention fromresearchers in different areas of mathematics and computer science andthis research will bring to light new connections them.In a wider context, the project concerns the fundamental relationshipunderlying models of computation on the one hand and logic on theother hand. The development of the theory of coalgebras opens up thepossibility of integrating existing insights and to explore newdirections.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.le.ac.uk