MURST - Programmi di ricerca scientifica di rilevante interesse nazionale Cofinanziamento'99.

Progetto TOSCA
Teoria della Concorrenza, Linguaggi di Ordine Superiore e Strutture di Tipi
Unita' di Genova

Last Updated 30 Nov 20001 by Eugenio Moggi.

Composizione (qualifica e mesi uomo)

E' inoltre previsto un assegnista di ricerca per 1 anno.

Afferenza a Tematiche del Personale strutturato

Il cognome CAPITALIZZATO indica afferenza principale ad una tematica

Compiti ed Obbiettivi

Lo scopo complessivo dell'unita` di ricerca di Genova e` l'identificazione, lo studio e l'applicazione di costrutti linguistici adatti ad una "violazione controllata" del "principio della scatola nera", cosi` che le scelte realizzative possano essere pianificate nel tempo oppure essere delegate ad un "livello meta". Un fine complementare e` la realizzazione di sistemi di tipi che garantiscano un "uso appropriato" dei costrutti linguistici. L'approccio generale consiste nello studio di tali costrutti in calcoli tipati (idealizzati) e nella verifica della loro utilita` per mezzo di proposte di prototipi di estensioni di linguaggi di programmazione esistenti. Il lavoro e` organizzato in quattro task specifici.

Linguaggi di moduli e sistemi di tipi per il riuso del codice

TEMATICA: 1 (ZuccaE, AnconaD). Collaborazioni esterne: ESPRIT WG APPSEM, Oregon Graduate Institute.

FASE 1. Definizione di un calcolo di ordine superiore per moduli mixin, dotato di un sistema di tipi e di una semantica per riduzione. Studio delle proprieta` di base e del potere espressivo. Realizzazione di un prototipo per un interprete di tale calcolo e per una estensione di Java con "classi mixin".

FASE 2. Estensione del calcolo dei moduli al caso di componenti di tipo, con definizioni mutualmente ricorsive, con possibile aggiunta di qualche forma di tipo manifesto e/o vincoli di tipo. Verra` inoltre considerato il livello di specifica, proponendo un'estensione di un linguaggio modulare orientato agli oggetti con moduli di specifica basati su interfacce Java arricchite con assiomi.

Tipi e costrutti per la manipolazione del codice

TEMATICA: 1, 6, 7 (MoggiE, CalcagnoC). Collaborazioni esterne: Oregon Graduate Institute.

FASE 1. Studio di linguaggi e modelli per la programmazione multi-stage, anche in presenza di effetti computazionali. Estensioni di linguaggi multi-stage che includano polimorfismo alla ML e/o operazioni aggiuntive sui tipi codice suggerite dalla sintassi astratta di ordine superiore.

FASE 2. Studio di linguaggi e sistemi di tipo che consentano la programmazione multi-stage in presenza di codice mobile. Verranno considerati sistemi di tipi piu` deboli, ad esempio "staged typing", se quelli proposti si rivelassero troppo restrittivi.

Incapsulamento di effetti computazionali

TEMATICA: 1, 6, 7 (MoggiE). Collaborazioni esterne: ESPRIT WG APPSEM, Oregon Graduate Institute.

FASE 1. Riformulazione piu` naturale, nel contesto di un linguaggio con "higher-order kinds", del meccanismo di incapsulazione monadica proposto da Launchbury e Peyton-Jones. Connessione piu' diretta con la nozione di "regione", usata nei "type and effect systems".

FASE 2. Estensione del meccanismo di incapsulamento ad altri effetti computazionali e studio delle analogie con la nozione di "molecola" nella Chemical Abstract Machine.

Riflessione computazionale e modellazione della comunicazione

TEMATICA: 1, 6 (AnconaM, CazzolaW) Collaborazioni esterne: Florida Atlantic University, Tsukuba University.

FASE 1. Estesione del modello riflessivo "channel reification", che supporta comunicazioni punto-a-punto, al fine di prevedere caratteristiche tipiche della comunicazione multi-punti (come il bilanciamento del carico di servizio). Definizione di una estensione di un linguaggio di programmazione orientato agli oggetti esistente che incorpori tale modello. Eventuali applicazioni a problematiche nell'ambito della sicurezza.

FASE 2. Realizzazione di un prototipo del nuovo linguaggio e confronto con altri meccanismi per la comunicazione distribuita, ad esempio RMI, multi-RMI e gruppi.