Is there a theory/abstraction behind OOP?

Functional programming has the very elegant Lambda Calculus and its variants as a backup theory. Is there such a thing for OOP? What is an abstraction for the object oriented model?

There are four main approaches, though these only scratch the surface of what is available:

• via lambdas and records: the idea is to encode objects, classes and methods in terms of more traditional constructs. Benjamin Pierce's work from the mid 90s is representative of this approach.

• Abadi and Cardelli's object calculi (see Abadi and Cardelli's book A Theory of Objects: their main abstraction is a record of methods, and the approach is closer to the prototype-based realisation of object-oriented programming, though classes and inheritance can be encoded in terms of the more primitive elements.

• Castagna's multimethod calculus (see Castagna's book Object-Oriented Programming A Unified Foundation): his approach takes multimethods are the key abstraction.

• Class-based calculi (such as in Kim Bruce's book Foundations of Object-oriented Languages: Types and Semantics or Featherweight Java): these approaches aim to capture the essence of class based programming and focus on classes and inheritance.

StackExchange Computer Science Q#18963, answer score: 16