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.
- Place
-
Ca' Vignal - Piramide,
Floor 0,
Hall Verde
- Programme Director
-
Ugo
Solitro
-
External reference
-
- Publication date
-
March 16, 2006