| EPSRC Reference: |
GR/R65190/01 |
| Title: |
Programming Logics for Denotations of Recursive Objects |
| Principal Investigator: |
Reus, Dr BG |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Engineering and Informatics |
| Organisation: |
University of Sussex |
| Scheme: |
Fast Stream |
| Starts: |
01 March 2002 |
Ends: |
30 April 2005 |
Value (£): |
62,363
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The aim of this project is to develop semantic models of objects that have enough properties to support a programming logic and to set up such a logic on denotations of objects in order to investigate its strengths and limitations. It is expected that the recursive character of objects and their specifications is much better understood on the denotational level.The project goals will be achieved by defining a realizability semantics of Abadi and Cardelli's functional object calculus in a direct style. By establishing proof principles for objects in the model one obtains a basic programming logic. These proof principles will be based on fixpoint induction or coinduction. It is investigated which interesting properties of object-based programs can be formulated and proved in this logic. Then the same procedure is to be repeated for a typed and an imperative version of the object calculus. The resulting logic shall then be used to verify a syntactic (Hoare-like) calculus for program verification in a direct style by using the denotational semantics of the language instead of the more syntactical operational semantics.Finally, if time permits, the results shall be transferred to class-based languages like Featherweight Java and ideally protoypically implemented by means of a theorem prover.
|
|
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.sussex.ac.uk |