| EPSRC Reference: |
EP/F042043/1 |
| Title: |
Linear Observations and Computational Effects |
| Principal Investigator: |
Simpson, Professor A |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Lab. for Foundations of Computer Science |
| Organisation: |
University of Edinburgh |
| Scheme: |
Standard Research |
| Starts: |
01 April 2008 |
Ends: |
30 April 2011 |
Value (£): |
346,830
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
24 Jan 2008
|
ICT Prioritisation Panel (Technology)
|
Announced
|
|
|
Summary on Grant Application Form |
|
Computational effects is a collective term for imperative aspects of computation, such as modifying state, raising exceptions, jumping, input/output, nondeterminism, etc., which together comprise a program's behaviour during execution. Typically, each occurrence of an effect is an individual event with its own identity. This separateness of distinct events is most naturally modelled using a special kind of linear logic which enforces the individuality of different occurrences. In this project we propose a canonical method of combining (a restricted but sufficiently expressive version of) such a linear logic with the standard mathematical machinery for modelling computational effects. An application will be to elucidate the nature of the linear usage of effects , whereby standard programming idioms ensure that the individuality of effects is respected.A second contribution is towards understanding the nature of behavioural equivalence between programs with effects. Whereas previously such equivalences have been axiomatized as basic, we instead implement them as observational equivalences , so programs are only distinguished if their observable behaviour differs. The novelty here is to build the notion of observation directly into the mathematical model, using it to determine all the other components usually required to model effects. This leads to new and rich mathematical models of effects, and also provides a basis for straightforward proofs of operational properties 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.ed.ac.uk |