EPSRC logo

Details of Grant 

EPSRC Reference: GR/N31672/01
Title: PRE-LOGICAL RELATIONS IN FIXPOINT CALCULI
Principal Investigator: Sannella, Professor D
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department: Sch of Informatics
Organisation: University of Edinburgh
Scheme: Standard Research (Pre-FEC)
Starts: 12 May 2000 Ends: 11 May 2001 Value (£): 4,500
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:  
Summary on Grant Application Form
Pre-logical relations are promising notion to formulate refinement. We have many examples, but we have not yet explored many areas of potential application. Hoare, He and Sanders introduced a particular pair of downward and upward simulations to give joint completeness result for relational semantics of nu-calculus. We first plan to investigate whether this pair of simulations is pre-logical relation for fixpoint calculi including mu-calculus. If so, we can obtain a single completeness result using the notion of pre-logical relation. If that is successful, we would proceed to investigate the nature of the conditions required for commands and simulations: in Hoare, He and Sanders work, these conditions are different and somewhat ad hoc: so we plan to clarify them in this pre-logical setting.
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.ed.ac.uk