| EPSRC Reference: |
GR/N22014/01 |
| Title: |
SEMANTIC APPROACHES TO CONTROL OF INTERFERENCE IN HIGHER-ORDER IMPERATIVE LANGUAGES |
| Principal Investigator: |
McCusker, Professor G |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Engineering and Informatics |
| Organisation: |
University of Sussex |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 June 2000 |
Ends: |
31 May 2003 |
Value (£): |
58,359
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| Information Technologies |
No relevance to Underpinning Sectors |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The aim of this project is to produce a semantic model for reasoning about interference in higher order programming languages, using game semantics. This will be achieved by first analysing and searching for models of existing mechanisms for control of interference, and then extending the new models obtained to incorporate additional features. Reynolds syntactic control of interference and its descendants can be seen as type systems built on top of a simple language called idealized algol. This simple language, without interference control a games model, so the first task will be adapt this model to take account of the ideas of syntactic control of interference. Other interference control systems, such as o-hearn and pyms alpha-lambda-calculus, will also be considered. The resulting models will be analysed, with a view to extending them to incorporate additional features, particularly pointers (general references). Again, a games model exists for an extension of idealized algol with pointers, which can serve as a starting point. No satisfactory syntactic interference control system yet exists for a language with pointers, sc our semantic approach will be used to explore the possibilities for defining such a system, the possibilities for developing proof techniques or static analysis algorithms based on the new games models will also be explored.
|
|
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.sussex.ac.uk |