| EPSRC Reference: |
GR/M21768/01 |
| Title: |
COMPUTATIONAL INVESTIGATION OF FULL INTUITIONISTIC LINEAR LOGIC |
| Principal Investigator: |
de Paiva, Dr V |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
School of Computer Science |
| Organisation: |
University of Birmingham |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 March 1999 |
Ends: |
29 February 2000 |
Value (£): |
45,394
|
| 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 |
|
Recently Linear Logic has been used to incorporate resource control into functional programming. This project proposes to use a variant of Linear Logic to incorporate a logical style of parallelism into functional programming. Thus we aim to construct the foundations for linear functional programming of an intrinsically parallel nature: the linear functional programming based on Full Intuitionistic Linear Logic (FILL). We want to establish the standard Curry-Howard correspondence between semantics, logic and programming language syntax which is the pre-requisite for any implementation of such a parallel language. The operators of FILL which model its intrinsic parallelism give rise to considerable difficulties when trying to extend the necessary results for the Curry-Howard correspondence to hold. Results similar to the ones we seek have so far been obtained only for traditional intuitionistic and intuitionistic linear logic. The fellow will concentrate on this correspondence between semantics and programming language syntax, building up from his previous doctoral work.
|
|
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.bham.ac.uk |