| EPSRC Reference: |
GR/R07615/01 |
| Title: |
Freshml: a Fresh Approach To Name Binding In Metaprogramming Languages |
| 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: |
30 June 2001 |
Ends: |
29 December 2004 |
Value (£): |
225,640
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
We propose to make a fundamental and rigorously founded extension to functional programming that will aid metaprogramming - the activity of creating software systems that manipulates syntactical structures (interprets, compilers, proof checkers, proof assistants, etc). In all but the most trivial cases, these syntactical structures involve variable binding, with associated notions of free and bound variables, renaming of bound variables, substitution of terms for free variables, and so on. It is generally agreed that this important aspect of presenting and computing with syntax is not catered for satisfactorily in existing functional programming languages commonly used for metaprogramming activities. Our recent theoretical work has thrown up promising new mathematical foundations for representing abstract syntax modulo renaming of bound names. The purpose of this proposal is to develop our new model; to design and implement FreshML, a functional programme language based on that model; and to discover, through experimentation, whether the model and programming language provide a useful idiom of metaprogramming tasks involving syntax with binders. FreshML, with is use of locally fresh names, pattern-matching on bound names in abstractions, and 'freshness inference' in its type system, will provide a fresh approach to computing with syntax modulo renaming of bound names that we will seek to integrate into the current state of the art in functional metaprogramming.
|
|
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.cam.ac.uk |