Abstract: Embedded specifications in object-oriented languages such as
   Eiffel are based on a rigorous approach towards validation,
   compatibility and reusability of sequential programs. Such
   specifications are not limited to functional and interface aspects but
   extend to complexity and, more generally, quantitative aspects in a
   straightforward way.
   
   However concurrent object-oriented languages are still in their
   infancy. Concurrent objects have inherently imperative facets, such as
   object identity, sharing and side-effects, that cannot be ignored in
   the semantics. Any marriage of objects and concurrency requires a
   trade-off in a space of desirable qualities whose dimensions are not
   completely independent.
   
   This paper summarises our work on a type system, calculus and an
   operational model for reasoning about concurrent objects. To achieve
   provability and efficiency, we are extending earlier work on
   sequential objects without adding concurrency control constructs.
   Instead types and interfaces are extended and induce a concurrent
   semantics of method implementations. This allows us to reason about
   stable compositions and correct implementation of concurrent objects.