| EPSRC Reference: |
EP/E056091/1 |
| Title: |
Semantics of Nondeterminism: Functions, Strategies and Bisimulation |
| Principal Investigator: |
Levy, Dr PB |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
School of Computer Science |
| Organisation: |
University of Birmingham |
| Scheme: |
Advanced Fellowship |
| Starts: |
01 January 2008 |
Ends: |
31 December 2012 |
Value (£): |
416,684
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
24 Apr 2007
|
ICT Fellowships 2007 - Interviews
|
FinalDecisionYetToBeMade
|
|
29 Mar 2007
|
ICT Fellowships Sift Panel
|
InvitedForInterview
|
|
|
Summary on Grant Application Form |
|
A key question in the theory of programming is: when are two programs equivalent? The answer will depend on what we think a program means. For example, we can think of a program as a function: the user gives all the required input, and then the computer behaves accordingly. Or we can think of it as a strategy for a game between the computer and the user: the computer gives some information, the user responds, the computer gives some more information, the user responds, and so on. These viewpoints have been extremely fruitful in recent years.To reason about a computer system, it is often necessary to idealize it as nondeterministic, i.e.\ possessing a range of possible behaviours. The factors that determine its actual behaviour are too low-level and complex to consider explicitly. But this apparently simple idea has ramifications for the theory of programming language semantics that are not well understood. They centre on the same questions: when are two programs equivalent, and what do programs mean? Previous research has used mathematical structures known from the theory of deterministic programs. But these have limited applicability to nondeterministic programs, and lead to somewhat awkward notions of equivalence. This research will proceed in the opposite direction: begin with certain computationally natural notions of equivalence, and investigate what structures they lead to. In some cases (thinking of programs as strategies), these are likely to be structures that we already know, but, by proceeding in this way, we aim to relate them more closely to the way programs actually behave.In other cases (thinking of programs as functions), completely new structures will be required. Some mysterious theorems have been proved that show that, in a sense, all programs (of a certain kind) share some behaviour---yet they do not tell us what this behaviour is. We will therefore undertake a careful examination of programs' behaviour to solve this mystery, and thereby obtain the required structures.
|
|
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.bham.ac.uk |