| EPSRC Reference: |
GR/R72259/02 |
| Title: |
Epigram: Innovative Programming via Inductive Families |
| Principal Investigator: |
Professor Z Luo |
| Other Investigators: |
|
| Researcher Co-investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Royal Holloway, Univ of London |
| Scheme: |
Standard Research |
| Starts: |
01 October 2004 |
Ends: |
31 August 2005 |
Value (£): |
50,483
|
| EPSRC Research Topic Classifications: |
| Information and communication technologies: Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary |
|
This is an adventurous proposal, seeking to investigate a novel approach to the practice of functional programming. We believe that a dependent type system centred on inductive families of datatypes can have a radical and positive impact on the way we define data structures and express computations over them. Inductive families are new to programming, and a distinct advance on the weaker technology made available by languages like DML, Cayenne and Haskell. Our objective is to demonstrate the value of this approach and make it accessible to programmers. Our method is to develop a platform, Epigram, and write programs: we will address substantial problems and compare our results with current practice. One of our case studies directly addresses a need for more informative data structures identified by our industrial collaborators, ALTA Systems (Northern Ireland) and our academic partners in the Centre for Educational Measurement at Queen's University, Belfast. Epigram is the first proposed platform to take inductive families seriously as data structures, and also the first to explore the benefits of dependent types for program code itself. This project is about learning to program in a new way.
|
| Final Report Summary |
|
This is an adventurous proposal, seeking to investigate a novel approach to the practice of functional programming. We believe that a dependent type system centred on inductive families of datatypes can have a radical and positive impact on the way we define data structures and express computations over them. Inductive families are new to programming, and a distinct advance on the weaker technology made available by languages like DML, Cayenne and Haskell. Our objective is to demonstrate the value of this approach and make it accessible to programmers. Our method is to develop a platform, Epigram, and write programs: we will address substantial problems and compare our results with current practice. One of our case studies directly addresses a need for more informative data structures identified by our industrial collaborators, ALTA Systems (Northern Ireland) and our academic partners in the Centre for Educational Measurement at Queen's University, Belfast. Epigram is the first proposed platform to take inductive families seriously as data structures, and also the first to explore the benefits of dependent types for program code itself. This project is about learning to program in a new way.
|
| Further Information: |
|
| Organisation Website: |
http://www.rhul.ac.uk |