| EPSRC Reference: |
EP/D000459/1 |
| Title: |
Computational Applications of Nominal Sets |
| Principal Investigator: |
Pitts, Professor AM |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science and Technology |
| Organisation: |
University of Cambridge |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 October 2005 |
Ends: |
30 September 2009 |
Value (£): |
86,224
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Computer scientists make use many different kinds of data structure associated with formal (i.e. precisely defined) languages. Software for constructing, analysing and transforming such data is widely needed, but is usually very complex and difficult to get correct. One reason for this is that computer languages often feature binding mechanisms for using temporary names for things, with the association of a name to the thing named only valid within a certain scope. Software for computing with formal languages should respect such binding structures; for example, it should not make any difference to the end result if a name is changed consistently throughout the scope of its binding (such changes are called alpha-conversions ). In systems for computing with formal languages it has proved very difficult to strike a good balance between providing users with unfettered access to the names of bound things while guaranteeing invariance under alpha-conversion. Nominal sets provide a new mathematical analysis of names and binding operations in formal languages with the potential to improve this situation. This project will investigate whether this new piece of mathematics can give rise to better computer systems for defining the meaning of programming languages and developing programs certified against the definition, in which the issues of names and binding are treated in a more expressive and user-friendly fashion than at present. The FreshML project in Cambridge has investigated this in the context of functional programming. We propose to extend this existing work in a new direction, by developing the equational logic of nominal sets, nominal term-rewriting, and associated algorithms (for unification, matching, residuation, narrowing, etc.). We aim to producing functional logic programming languages and machine-assisted theorem provers supporting forms of structural recursion and induction modulo alpha-conversion that remain faithful to informal practice.
|
|
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: |
http://www.dcs.kcl.ac.uk/staff/maribel/CANS/ |
| Further Information: |
|
| Organisation Website: |
http://www.cam.ac.uk |