There is considerable commercial interest in object-oriented (OO) systems. These are normally implemented in C++, a language that many theoretically inclined academics consider ad hoc and messy. To try to improve the situation, there is much research into cleaner alternatives to C++ like Modula-3 (which is taught at Cambridge), SELF [10] and Obliq, and the theoretical concepts needed to support them. Also, some work [9] reported in the 1994 ML workshop has been done on using Standard ML to encode object-oriented programming idioms.
Quite a bit of research concerns the soundness, completeness, decidability etc. of various type systems for object-oriented programming. Many of the proofs appear to be complicated and intricate and so might be worth checking mechanically.
A (somewhat randomly chosen) recent paper in this area is A Lambda Calculus of Objects and Method Specialization [2]. The abstract of this is:
This paper presents an untyped lambda calculus, extended with object primitives that reflect the capabilities of so-called delegation-based object-orirented languages. A type inference system allows static detection of errors, such as message not understood, while at the same time allowing the type of an inherited method to be specialized to the type of the inheriting object. Type soundness is proved using operational semantics and examples illustrating the expressiveness of the pure calculus are presented.
It would be interesting to formalize the calculus and then mechanically check the proofs in the paper.
A more applied project would be to take a semantically tractable object-oriented programming language and to develop formal specification and verification tools for it. For example, Obliq is an implemented experimental language developed by Luca Cardelli at Digital's System Research Center (SRC). It is based on clean mathematical foundations developed by Luca Cardelli and Martìn Abadi.
Cardelli describes Obliq as follow:
Obliq is a lexically-scoped untyped interpreted language that supports distributed object-oriented computation.An Obliq computation may involve multiple threads of control within an address space, multiple address spaces on a machine, heterogeneous machines over a local network, and multiple networks over the Internet.
Obliq objects have state and are local to a site. Obliq computations can roam over the network, while maintaining network connections.
A possible project would be to investigate providing a semantic embedding of Obliq (or its underlying calculus) into Isabelle or HOL. This could then be used for various purposes including reasoning about the language itself (proof of meta-properties) and reasoning about individual programs.
I don't know much about object orientation, so the suggestions above are certainly half-baked and might be totally loony. However, Benjamin Pierce, a leading researcher in theoretical aspects of object-oriented type systems, is coming to Cambridge with Robin Milner. If there were interest in applications of automated reasoning to object-oriented systems then a combination of Mike Gordon/Larry Paulson (for AR) with him (for OO) might be possible.
A rather different area is providing mechanical support for object-oriented specification languages like Object-Z. My own feeling is that one needs to first sort out ordinary Z, which is discussed further in Section 3.6.