| EPSRC Reference: |
GR/S30450/01 |
| Title: |
Extensions of Dependent Type Theory - Induction, Interaction, Universes |
| Principal Investigator: |
Setzer, Dr A |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Swansea University |
| Scheme: |
First Grant Scheme Pre-FEC |
| Starts: |
01 October 2003 |
Ends: |
30 November 2006 |
Value (£): |
123,028
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Dependent type theory extends the usual type systems in programming languages by allowing data types to depend on programs. The resulting type theory is much more expressive and allows to specify the correctness of programs as types. Restrictions of such type theories (templates) are currently investigated in generative programming. The goal of this project is to carry out fundamental research on extensions of dependent type theory in order to develop a theoretical basis for its use as a practical programming language: I) To intensify our understanding of interactive programs in dependent type theory developed by us and P. Hancock. Especially we want to investigate state dependent 10, in which interactive commands depend on previous ones, generalize this concept to general coalgebras,i and work on case studies, correctness and parallelism. If) To develop concepts from objectoriented programming in dependent type theory and investigate applications in component based software construction. III) To study inductive-recursive definitions and their applications in generic programming. The basis is our formulation of inductive-recursive definitions, which provides a powerful data type with codes for the majority of data types used in programming, including all algebraic data types and function types. IV) To develop extensions of dependent type theory, the strength of which is substantially stronger than the known versions of type theory, and to measure their strength.
|
|
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.swan.ac.uk |