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

Speaker:  Ugo de' Liguoro - Università di Torino
  Friday, March 24, 2006 at 11:00 AM
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.

Ca' Vignal - Piramide, Floor 0, Hall Verde

Programme Director
Ugo Solitro

Publication date
March 16, 2006