# EP/E056091/1 - Semantics of Nondeterminism: Functions, Strategies and Bisimulation

Research Perspectives grant details from EPSRC portfolio

EPSRC Database

Source RCUK EPSRC Data

Research Perspectives grant details from EPSRC portfolio

Principal Investigator - School of Computer Science, University of Birmingham

Start Date

01/2008

End Date

12/2012

Value

£416,684

Similar Grants

Automatic generation of similar EPSRC grants

Similar Topics

Topic similar to the description of this grant

Grant Description

Summary and Description of the grant

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.

EPSRC Grants On The Web Link

http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/E056091/1

Structured Data / Microdata

Grant Event Details:

Name: Semantics of Nondeterminism: Functions, Strategies and Bisimulation - EP/E056091/1

Start Date: 2008-01-01T00:00:00+00:00

End Date: 2012-12-31T00:00:00+00:00

Organization: University of Birmingham

Description: 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 ...