| EPSRC Reference: |
EP/F042337/1 |
| Title: |
Formalisms for Structural Operational Semantics |
| Principal Investigator: |
Klin, Dr B |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science and Technology |
| Organisation: |
University of Cambridge |
| Scheme: |
Postdoc Research Fellowship |
| Starts: |
01 May 2008 |
Ends: |
30 April 2011 |
Value (£): |
216,634
|
| 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 |
|
Operational semantics is a formal method of describing the meaning and behaviour of programming languages. Such methods are needed for automated program analysis, verification, translation or even construction. An operational specification describes how programs can perform actions and, at the same time, transform to other programs. Language designers have a wide choice of formalisms for writing operational descriptions of programs. In the so-called structural approach, the actions that a program may take are determined by the actions of its subprograms. In the reactive approach, program statements are thought to communicate with one another throughout the program structure to decide on the next action to take. The chosen formalism also depends on the kind of computational features used in the language, such as nondeterminism, probabilistic choice, real time, store, input/output, etc.Such a wide choice is welcome, but it can also be problematic. The large number of possible formalisms means that some of them are less thoroughly studied than other ones, and indeed it often happens that language designers create ad-hoc formalisms of their own, tailored to the needs of particular languages. They are then forced to check that their new formalism is meaningful and well-behaved, i.e., that it guarantees certain desirable properties of programs and facilitates reasoning about them.We aim at relieving language designers from some of this burden by developing a systematic, general approach to formalisms for operational semantics. We will study mathematical theories of both the structural and the reactive approach, aiming at a general theory of operational specifications. Such a theory will benefit programming language designers, facilitating the creation of new languages, the modification of existing ones, and the analysis of programs.
|
|
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.cam.ac.uk |