Formal derivation of program properties for object-based languages. A logical interpretation of Subtyping.

Using Abadi and Cardelli typed sigma-calculus as a model of object based programming languages, we introduce a formal system to derive program properties. The system induces a notion of equivalence, which is based on logical indiscernibility, on turn depending on types. We show that the equivalence is a model of Abadi and Cardelli axiomatic theory of objects; that it is computationally adequate (in the sense that neither differenet atomic values are identified, nor converging and diverging programs do), and more importantly that we obtain a natural interpretation of subtyping, in terms of (reverse) inclusion of logical theories.