Formal techniques for parallel object-oriented languages

This paper is intended to give an overview of the formal techniques that have been developed to deal with the parallel object-oriented language POOL and several related languages. We sketch a number of semantic descriptions, using several formalism: operational semantics, denotational semantics, and a new approach to semantics, which we call layered semantics. Then we summarize the progress that has been made in formal proof systems to verify the correctness of parallel object-oriented programs. Finally we survey the techniques that we are currently developing to describe the behaviour of objects independently of their implementation, leading to linguistic support for behavioural subtyping.