Relatore:
Ugo de' Liguoro
- Università di Torino
venerdì 24 marzo 2006
alle ore
11.00
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.
- Luogo
-
Ca' Vignal - Piramide,
Piano 0,
Sala Verde
- Referente
-
Ugo
Solitro
-
Referente esterno
-
- Data pubblicazione
-
16 marzo 2006