| EPSRC Reference: |
GR/L38356/01 |
| Title: |
AN OPERATIONAL THEORY OF OBJECTS |
| Principal Investigator: |
Pitts, Professor AM |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science and Technology |
| Organisation: |
University of Cambridge |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 February 1997 |
Ends: |
31 January 2000 |
Value (£): |
167,756
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The goal of this project is to develop formal foundations and verification methods for object-oriented languages, and hence to increase confidence in their design, implementation and use. We will exploit recent mathematical advances that support proof of program priorities directly from the operational semantics of a language. We will transfer techniques developed first for lambda calculus and ML to an object-oriented setting. The setting of objects both increases the possible applications of these techniques and poses a range of new technical challenges such as the encapsulation of state and self-application semantics of method invocation. We will work within the family of object calculi recently developed by Abadi and Cardelli at DEC SRC. An object calculus is a formalism similar to lambda calculus, but based exclusively on objects rather than functions. Because they focus on a few fundamental features, such as method invocation, subtyping and polymorphism, object calculi make a more realistic and longer lasting setting for semantics research than any full-blown language. the project will apply operational techniques to a range of functional, imperative and concurrent object calculi and evaluate these techniques via implementation work and feasibility studies involving compiler optimisations and mechanised verification of type systems.
|
|
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.cam.ac.uk |