Formal proof of the semantic equivalence between the core of the AOP language AspectTalk and the OOP language Smalltalk

Denotational semantics of programming languages are considered. The core of an aspect-oriented programming language is defined as its subset which is not aspect-oriented. Semantics equivalence between the core of the aspect-oriented programming language AspectTalk and the object-oriented programming language Smalltalk is proven with commutativity of the diagram in which objects are syntax or semantic domains and arrows are homomorphisms. The proof shows in particular that the core of AspectTalk is really an object-oriented programming language and the automatic translation of programs from the core of AspectTalk into Smalltalk and vice versa is possible.