Derivazione formale di proprietà di programmi object-based ed un'interpretazione logica del subtyping.

Utilizzando il sigma-calcolo tipato di Abadi e Cardelli come modello formale dei linguaggi di programmazione object-based fortemente tipati, si introduce un sistema per la derivazione formale di proprietà dei programmi. Il sistema induce una nozione di equivalenza basata sul principio degli indiscernibili, la quale dipende dal tipo dei termini.
Si dimostra che questa nozione è un modello della teoria assiomatica degli oggetti proposta da Abadi e Cardelli; che è computazionalmente adeguata (nel senso che non identifica programmi divergenti con altri che non lo sono, ed anzi caratterizza i primi), ma soprattutto che fornisce un'interpretazione naturale della nozione di sottotipo, in termini di inclusione (inversa) di teorie logiche.