| EPSRC Reference: |
GR/H77545/01 |
| Title: |
DEFINITIONAL CONSTRAINT PROGRAMMING: A FOUNDATION FOR LOGICALLY CORRECT CONCURRENT SYSTEMS |
| Principal Investigator: |
Darlington, Professor J |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computing |
| Organisation: |
Imperial College London |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 August 1992 |
Ends: |
31 July 1995 |
Value (£): |
128,072
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The theme of this research project is the development of a secure foundation for declarative concurrent programming based on the integration of the logic and constraint computational models, and to build on this foundation a multi-paradigm programming system which unifies a series of, currently separate, existing research themes including concurrent constraint programming, parallel functional programming and process calculi.Progress:Theoretical Results:Logical Process Calculus: One of the major theoretical achievements of the project is the development of a logical process calculus as a uniform linguistic and semantic framework for studying the behaviour of concurrent processes. The calculus itself can be regarded as a definitional constraint programming (DCP) system where linear logic is employed as the underlying logic. We have established a natural way to code the essential behaviours of concurrent computation into linear logic. Various concurrent computational models including data flow, graph reduction, actors, parallel functional programming and the p-calculus have been formalised and studied in this calculus. We have published 4 papers on the research results of the calculus.l-Calculus with Logical Variables: From the logical process calculus we have developed a version of the l-Calculus with logic variables, called the LV-calculus, as a theoretical foundation for parallel functional languages. A concurrent reduction model has been proposed for the calculus which provides a precise formalisation of the lenient reduction strategy used in Id and parallel Haskell to evaluate parallel functions. A significant innovation of the calculus is the introduction of the lazy consistency check mechanism. This provides a new form of lazyness to resolve the higher order unification problem in the calculus. We have published 2 papers on this research. Practical Results: A Concurrent Definitional Constraint Language: Based on the theoretical research, we have designed, in cooperation with researchers at TU Berlin, a concrete DCP language, named Goffin, for declarative parallel programming. The language applies constraints to form a co-ordination system organising the concurrent interaction of parallel functional computations. We have written 3 papers on the design and implementation of this language. A General Purpose Parallel Co-ordination Language: One of the practical applications of the research results has been a general purpose parallel co-ordination language, SCL (Structured Composition Language), applying the DCP model for structured parallel programming. This research integrates our project with our other, long standing, research on skeleton-based parallel programming. The recent development of the SCL system applies constraints and parallel functions to define skeletons as the uniform means to abstract all aspects of the parallel behaviour of programs. Based on the skeleton approach of abstracting parallel computational patterns, we have achieved a new structured parallel programming framework, SPP(X). In this scheme, parallel programs can be constructed by composing the sequential procedures written in a conventional base language according to user defined parallel structures. We have published 3 papers on this research. The initial results of this research have already attracted interest in both academia and industry.
|
|
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.imperial.ac.uk |