|
| EPSRC Reference: |
GR/S86372/01 |
| Title: |
A Theory of Effects for Programming Languages |
| Principal Investigator: |
Professor G Plotkin |
| Other Investigators: |
|
| Researcher Co-investigator: |
| Dr A Power |
Professor P Wadler |
|
|
| Project Partner: |
|
| Department: |
Sch of Informatics |
| Organisation: |
University of Edinburgh |
| Scheme: |
Standard Research |
| Starts: |
01 March 2004 |
Ends: |
30 April 2008 |
Value (£): |
430,332
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary |
|
We intend to make progress using the idea of algebraic operations for constructing effects (example: fair probabalistic choice) and their correlates, generic effects (example: fair random coin toss). We previously gave a uniform operational semantics for finitary such effects and a theory of modularity for most global effects (no declarations). We will complete these theories, accounting for state-oriented operational semantics and modularity for nondeterminism and local effects. We will also: treat control effects; provide a theory of effect observation for operator equations, and notions of contextual program equivalence; give a uniform treatment of language technologies such as effect systems; and provide an expressive and far-reaching logic of effects.
|
| Final Report Summary |
We progressed using the idea of algebraic operations for constructing effects (for example: fair probabalistic choice) and their correlates, generic effects (for example: fair random coin toss). We previously gave a uniform operational semantics for finitary such effects and a theory of modularity for most global effects (no declarations). We completed, or partially completed, these theories, giving a co-algebraic account of state-oriented operational semantics configurations; accounting for modularity for nondeterminism by a novel distributive combination of equational theories, complementing the two previous methods; and beginning an account of local effects by giving a construct that extends global computational effects canonically to a corresponding local computational effect (but there remains the problem of finding notions of algebraic and equational theories for local effects).
We also treated control effects, giving an axiomatic notion of the combination of continuations with other effects with good modularity properties. We provided a general logic of effects that uniformly incorporated Scott and Milner's LCF with modal logics, such as Hennessy-Milner logic, and with Moggi and Pitt's evaluation logic; it remains to add state but we are optimistic that the co-algebraic methods, referred to above, will provide the way forward. In so doing, we transitioned from a call-by-value approach to a call-by-push-value approach, a la Levy, that incorporates both call-by-value and call-by name It remains to add recursive types: that should be straightforward at the language level, but brings into question how to extend the current logic, and particularly how to give an acceptable treatment of admissible logical relations.
We researched the combination of ordinary and probabilistic nondeterminism, contributing to the programme of a domain-theoretic functional analysis; we also considered the interaction of effects and domain theory, particularly whether the algebraic methods still applied in a non-standard domain-theoretic context that also provides for polymorphism. We looked at various aspects of logical frameworks including a categorical treatment of general contexts using higher-order monads and beginning a programme of algebraic type-theory. Both of these are needed for the programme of a general logic of effects: the first to treat local effects and the second to treat parameterised infinitary theories in a finitistic way. Progress was made on the algebraic treatment of effect deconstructors such as exception-handling mechanisms. Our idea is to treat them as constructions of non-free algebras together with a homomorphic extension of a map from values to one on a free algebra. Finally, categorical algebra has provided much of the mathematical foundation of our work and effort went into its further development.
|
| Further Information: |
|
| Organisation Website: |
http://www.ed.ac.uk |
|
|