|
| EPSRC Reference: |
EP/C512022/1 |
| Title: |
Observational Equality For Dependently Typed Programming |
| Principal Investigator: |
Dr T Altenkirch |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
School of Computer Science |
| Organisation: |
University of Nottingham |
| Scheme: |
Standard Research |
| Starts: |
01 December 2004 |
Ends: |
31 May 2008 |
Value (£): |
242,198
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary |
While dependent types have been used in theorem proving for quite some time, dependently typed programming is an emerging field, enriching conventional programming with a powerful type discipline, which enables programmers to express properties of a program in its type. New software development tools like Epigram (EPSRC GR/R 72259), developed by McBride, based on dependent types can be used to engineer software which is correct by construction - this can be checked by the compiler. The Epigram system is available from htto://www.dur.ac.uk/CARG/epigram/.
One of the main bottlenecks for the successful employment of this technology is the treatment of equality. Present systems are either extensional or intensional, with different advantages and disadvantages: intentional systems allow us to implement an automatic type checker but do not identify programs which have the same behaviour, extentional systems do this, but type checking requires theorem proving. In 1999 Altenkirch published a paper, showing that, in principle, it is possible to combine the advantages of both approaches.
We intend to reap the fruits by turning theory into practice: we plan to turn Altenkirch's theoretical proposal into a calculus which will form the base of a new tool, Observational Epigram. The main focus of the project is to provide positive proof of the benefits gained:
1. a small fixed core Epigram's language of data structures and programs will become reducible to a small fixed language, ideal for communication of reliable code across networks - independent client-side rechecking will be simple.
2. extensible typechecking Using extensional equality we can improve the automation of type checking using Epigram programs provided by the programmer. We have identified a realistic PhD project in this area.
3. natural reasoning about real systems Extensional equality is essential when implementing systems with an infinite behaviour such as physical control systems, network routers or window systems. We plan to show by selected case studies that Observational Epigram can become a practical tool for mechanically certified software engineering in the real world.
.Dr Altenkirch and Dr McBride have a well-established record of fruitful collaboration; Dr Altenkirch's PhD students use Epigram intensively. Between us, we have the theoretical skills and the practical craft to deliver on this agenda.
|
| Final Report Summary |
While dependent types have been used in theorem proving for quite some time, dependently typed programming is an emerging field, enriching conventional programming with a powerful type discipline, which enables programmers to express properties of a program in its type. New software development tools like Epigram (EPSRC GR/R 72259), developed by McBride, based on dependent types can be used to engineer software which is correct by construction - this can be checked by the compiler. The Epigram system is available from htto://www.dur.ac.uk/CARG/epigram/.
One of the main bottlenecks for the successful employment of this technology is the treatment of equality. Present systems are either extensional or intensional, with different advantages and disadvantages: intentional systems allow us to implement an automatic type checker but do not identify programs which have the same behaviour, extentional systems do this, but type checking requires theorem proving. In 1999 Altenkirch published a paper, showing that, in principle, it is possible to combine the advantages of both approaches.
We intend to reap the fruits by turning theory into practice: we plan to turn Altenkirch's theoretical proposal into a calculus which will form the base of a new tool, Observational Epigram. The main focus of the project is to provide positive proof of the benefits gained:
1. a small fixed core Epigram's language of data structures and programs will become reducible to a small fixed language, ideal for communication of reliable code across networks - independent client-side rechecking will be simple.
2. extensible typechecking Using extensional equality we can improve the automation of type checking using Epigram programs provided by the programmer. We have identified a realistic PhD project in this area.
3. natural reasoning about real systems Extensional equality is essential when implementing systems with an infinite behaviour such as physical control systems, network routers or window systems. We plan to show by selected case studies that Observational Epigram can become a practical tool for mechanically certified software engineering in the real world.
.Dr Altenkirch and Dr McBride have a well-established record of fruitful collaboration; Dr Altenkirch's PhD students use Epigram intensively. Between us, we have the theoretical skills and the practical craft to deliver on this agenda.
|
| Further Information: |
|
| Organisation Website: |
http://www.nott.ac.uk |
|
|