A Denotational Approach for Type-Checking in Object-Oriented Programming Languages

Starting with a pragmatical (but formal) definition of type in object-oriented languages, this paper proposes a method to test type safety in this kind of language. We say that a language is (type) safe if it ensures that, during the execution of a correct program, every message sent to an object is matched by an appropriate method. We define a "typical" object oriented programming language, featuring multiple inheritance, recursive types, and separation between specifications and implementations. Then, we give a formal definition for its type system, and a denotational semantics for the execution of the language, based on message passing. Finally, we formally prove that our language is type safe. Along the work, better understanding is gained about many problems related with type systems in object-oriented languages. Keywords: Semantics of Programming Languages, Type Systems, Object Oriented Programming. 1 Introduction In recent years, there has been a great interest in type systems..