| EPSRC Reference: |
GR/M98555/01 |
| Title: |
MECHANIZED OPERATIONAL SEMANTICS |
| Principal Investigator: |
Crole, Dr R |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Mathematics |
| Organisation: |
University of Leicester |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 July 2000 |
Ends: |
30 September 2003 |
Value (£): |
151,724
|
| 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 |
|
The aim of the project is to investigate the viability of using a theorem prover for reasoning about programming language properties in general, and compiler optimisations in particular. The project will be a large scale development of both the theory and practice of computer aided (or mechanised) reasoning and will deliver an end product of a monadic calculus for analysing compiler optimisations, together with a library of tools for syntax representation and tactical verification for:a) the specification of program syntax and semantics of a (functional) higher order imperative language, ML-small, at varying levels of abstraction and detail:b) formal verification of the relative correctness of such semantics:c) proofs of language properties, such as type soundness: andd) proofs of equivalences of program code, and correctness of compiler optimisations.While the entire programme will be of general interest to language designers and compiler writers, it is the compiler optimisation proofs which may have the most direct payoffs. We will be providing a framework in which the details of such optimisations can be studied effectively, potentially producing results which could have an impact on real compilers.
|
|
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.le.ac.uk |