| EPSRC Reference: |
GR/M75518/01 |
| Title: |
AN OPEN PROOF CHECKER BASED ON TYPE THEORY |
| Principal Investigator: |
Luo, Professor Z |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Durham, University of |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 August 1999 |
Ends: |
31 December 2002 |
Value (£): |
268,300
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
This project will build on the proposers' deep experience in the type theory and proof checker implementation to develop a new type theory and a prototype implementation. We want to support openness for modification of both the underlying type theory and the implementation, particularly to allow interaction with other reasoning tools such as model checkers and computer algebra systems. Our approach has two parts:1. Make the type theory simpler so it can be implemented directly from its formal definition, and2. Build the proof checker on software engineering principles. The new type theory, based on recent developments in type theory, will also address issues not well handled by present implemented type theories: e.g. pattern matching, subtyping, existential variables, proof modularity, and object language computation. This work will result in both published articles about type theory and a working prototype implementation.
|
|
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: |
|