| EPSRC Reference: |
EP/G034109/1 |
| Title: |
Reusability and Dependent Types |
| Principal Investigator: |
Altenkirch, Dr T |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
School of Computer Science |
| Organisation: |
University of Nottingham |
| Scheme: |
Standard Research |
| Starts: |
01 March 2009 |
Ends: |
28 February 2013 |
Value (£): |
244,671
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
01 Dec 2008
|
ICT Prioritisation Panel (December 2008)
|
Announced
|
|
|
Summary on Grant Application Form |
|
Robin Milner coined the slogan well typed programs cannot gowrong , advertising the strength of typed functional languages like MLand Haskell in using types to catch runtime errors. Nowadays, we canand want to go further: dependently typed programming exploits thepower of very expressive type systems to deliver stronger guaranteesbut also additional support for software development, using types toguide the development process. This is witnessed by a recent surge oflanguage proposals with the goal to harness the power of dependenttypes, e.g. Haskell with GADTs, Agda, Coq, Omega, Concoqtion, Guru,Ynot, Epigram and so on.However, expressive type systems have their price: more specific typesfrequently reduce the reusability of code, whose too-specificimplementation type may not fit its current application. Thisphenomenon already shows up in the traditional Hindley-Milner styletype system of ML and Haskell; it becomes even more prevalent in adependently typed setting. Luckily, all is not lost: dependent typesare expressive enough that they can talk about themselvesreflectively, making meta-programming one of its potential killerapplications with the potential of combining expressive types andreusable software components.Based on and inspired by recent research at Nottingham on dependentlytyped programming (EPSRC EP/C512022/1) and container types (EPSRCEP/C511964/2) and at Oxford on datatype-generic programming (EPSRCGR/S27078/01, EP/E02128X/1) we plan to explore the potential ofdependent types to deliver reusable and reliable softwarecomponents. To achieve this, we intend to explore two alternativeroads - reusability by structure and reusability by design - andexpress both within a dependently typed framework. Our programme is tobuild new tools extending the Epigram 2 framework, investigate theunderlying theory using container types, and most importantlyestablish novel programming patterns and libraries. We seek fundingfor an RA at Nottingham (Peter Morris, whose PhD laid much of thegroundwork for this proposal), and two doctoral students (one each atOxford and Strathclyde), together with appropriate support forequipment, coordination, travel, and dissimination (i.e. a workshopand a summer school)
|
|
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.nottingham.ac.uk |