Article snapshot taken from[REDACTED] with creative commons attribution-sharealike license.
Give it a read and then ask your questions in the chat.
We can research this topic together.
Abadi tried to give an example of pure object-oriented language which would allow studying the formal semantics of objects. "Baby Modula-3 is defined with a structured operational semantics and with a set of static type rules. A denotational semantics guarantees the soundness of this definition."
This object model has been shown to have well definiteness decidability (a mechanical proof of it isn't known).
Luca Cardelli and Martín Abadi wrote the book A Theory of Objects in 1996, laying out formal calculi for the semantics of object-oriented programming languages. Baby Modula-3 influenced this work according to Cardelli, and guided a calculus of the type of self in Types for object and the type of 'self'.
It has opened the way for work on Modula-3 formal semantic checking systems, for object-oriented type system programming languages that have been used to model the formal semantics of languages such as Ada and C.
Schwinghammer, J. (2008-01-01). "On Normalization by Evaluation for Object Calculi". In Miculan, Marino; Scagnetto, Ivan; Honsell, Furio (eds.). Types for Proofs and Programs. Lecture Notes in Computer Science. Vol. 4941. Springer Berlin Heidelberg. pp. 173–187. CiteSeerX10.1.1.140.5764. doi:10.1007/978-3-540-68103-8_12. ISBN978-3-540-68084-0.