Cardelli is a highly reputed academic. That book is a pretty seminal book, lots of papers refer to it.

I'm also not really sure what you're trying to point out. When you talk about a calculi for FP, you're talking about what? Lambda Calculus?

If so, the base mathematical model of OOP is the Turing machine. That's the model of computation involved. It's been extensively researched and is absolutely well accepted and recognised by everyone everywhere.

Similarly to how there was no mathematical model of Haskell or Idris, etc. There wasn't any for OOP languages either like Java, C++, etc. Any attempt at a mathematical framework over those languages came after, and none of them have a strong one that I know off. Some of them, maybe most especially Idris, did get a lot of inspiration from known typing mathematical models, but still the language itself does not have a full on calculus of itself (correct me if I'm wrong)

If you're talking about type theory and type systems as related to provability of computation, that's like a whole other conversation. But even then, there's ton of literature that research type systems that can prove OOP, often focused on subtyping since that's the main typing discipline of most OO languages with static type systems.