| EPSRC Reference: |
GR/M56333/01 |
| Title: |
THE STRUCTURE OF PROGRAMMING LANGUAGES: SYNTAX AND SEMANTICS |
| Principal Investigator: |
Plotkin, Professor G |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Informatics |
| Organisation: |
University of Edinburgh |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 March 1999 |
Ends: |
31 March 2003 |
Value (£): |
530,319
|
| 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 |
|
The main goal of the proposed research is to achieve an effective theory of programming languages, particularly, their syntax and semantics: both operational and denotational. A subsidiary goal is the understanding of logic formalisms for program specification, correctness and development. The proposed research is foundational, aimed at a mathematical framework for formal methods and, more generally, applied formalisms in software engineering; both general and particular, ranging from general accounts of syntax and semantics to investigations of individual programming phenomena; and, to achieve effectiveness, strongly oriented to formalisms.To obtain an effective theory, we concentrate on core issues. Existing theories of abstract syntax are inadequate; we will develop improved algebraic theories, covering variable binding and structured types. For operational semantics we seek a general theory not tied to syntactic presentation, using co-algebras and distributive laws. Combining these yields a useful global bialgebraic view of programming languages. Computational effects underline semantics. Here Moggi's monadic approach needs strengthening in several aspects e.g., operational semantics and modularity. Linear type theories, arising from aximatic domain theory, may yield a further improvement, incorporating an integrated treatment of parameter-calling mechanisms. There will also be some work on generic logic, computational logics, and combined formalisms for program development.
|
|
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 |