| EPSRC Reference: |
GR/K79130/01 |
| Title: |
SUBTYPING, INHERITANCE AND REUSE: DEVELOPING EXPRESSIVE TYPE THEORY FOR FORMAL ANALYSIS |
| 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 October 1996 |
Ends: |
29 February 2000 |
Value (£): |
138,483
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Formal analysis based on proof development systems often involves large formal development. Effective reuse of developed formal theories and proofs is essential for formal analysis of large systems to become efficient. Current type theories and the associated theorem provers lack the expressive power and do no not support direct inheritance. This project will be to develop new subtyping mechanisms for expressive type theory and the associated inheritance-based methods to support structuring and reuse of formal theories in proof development. The type theory developed in our previous work and implemented in the Lego proof development system will be extended with suitable subtyping mechanisms and implemented to support practical applications based on inheritance structuring and reuse methods. The implementation and methods will be applied to case study and used to build a library of formal theories to be exploited by the users in applications. The major contribution of the research are: further development of expressive type theory with subtyping and inheritance mechanisms; better understanding of theory structuring and reuse in formal analysis; practical support for efficient analysis of large systems to obtain sealability.
|
|
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: |
|