Objects and Classes in Algol-like Languages 1

Many object-oriented languages used in practice descend from Algol. With this motivation, we study the theoretical issues underlying such lan-guages via the theory of Algol-like languages. It is shown that the basic framework of this theory extends cleanly and elegantly to the concepts of objects and classes. Moreover, a clear correspondence emerges between classes and abstract data types, whose theory corresponds to that of exis-tential types. Equational and Hoare-like reasoning methods, and relational parametricity provide powerful formal tools for reasoning about Algol-like object-oriented programs. Key Words: Algol-like languages, relational parametricity, specication logic, object-oriented programming, semantics