Last updated 12/02/1999 by Eugenio Moggi.

Unita' di Genova, Linguaggi Funzionali

Risultati di maggior rilievo conseguiti nel corso dell'attivita di ricerca

Relazione con la tempistica iniziale del programma

Si sono rispettate le tempistiche previste per la prima fase. Si pensa di rivedere gli obbiettivi della seconda fase per continuare l'attivita' iniziata con [MTBS98].

Corrispondenza con i criteri di verificabilita` enunciati nella proposta originale

I lavori relativi agli obbiettivi per la prima fase sono: [Mog98], [Cal98]. Nel corso del primo anno ci si e' resi conto che le semantiche sviluppate nel progetto potevano avere un impatto molto rilevante per lo sviluppo di linguaggi multi-stage. A seguito di cio' si e' deciso di ridirigere il campo di applicazione, cio' ha dato luogo ad una collaborazione con OGI, che ha portato ad articolo [MTBS98]. I seguenti lavori sono invece preliminari agli obbiettivi per la seconda fase: [BJM98], [BJM98b].

Carattere innovativo in rapporto allo stato dell'arte nel campo

[Mog98] introduce un approccio innovativo alla modellazione dei linguaggi a due-livelli, che evita i difetti delle semantiche denotazionali proposte in precedenza. [Cal98] affronta tematiche tradizionali, che non erano state esaminate nel contesto dei linguaggi a due-livelli. [MTBS98] e' altamente innovativo, e propone il primo linguaggio in cui si puo' manipolare sia codice chiuso (p.e. per run-time code generation) che codice aperto (con tecniche di partial evaluation).

Resoconto primo Anno (01/02/1998 - 31/01/1999)

[Mog98] propone una semantica per linguaggi a due-livelli basata sulle categorie di funtori. Rispetto ad altre semantiche denotazioni si ha una maggiore astrazione (gli elementi del tipo code sono programmi modulo alfa-conversione) e vale un risultato di full-abstraction limitatamente ai tipi dinamici. La dimostrazione di correttezza rispetto ad una semantica standard usa le logical relations a la Kripke, ed evita gli errori ed imprecisioni presenti nelle dimostrazioni di correttezza pubblicate in precedenza. Sebbene il linguaggio considerato e' particolarmente semplice (si tratta di lambda-mix), la semantica sembra facilmente estendibile a liguaggi piu' complessi.

[Cal98] analizza le relazioni tra semantica operazionale, semantica denotazionale e calcolo equazionale per una variante di PCF a due-livelli. Questo tipo di analisi e' tipica dei linguaggi di programmazione. Nel contesto dei linguaggi a due-livelli vi sono varie osservazioni possibili. L'articolo prendere come osservazioni base due tipi di terminazione, quella a tempo di compilazione e quella a tempo di esecuzione, e dimostra che vale un risultato di adequatezza computazionale per due semantica denotazionali, una in CPO e l'altra in CPO^2 (che ricade nel framework proposto in [Mog97]).

[MTBS98] e' il frutto della collaborazione con ricercatori dell'Oregon Graduate Center che da tempo si occupano di linguaggi per computazioni multi-stage. Il linguaggio proposto, AIM, e' il primo tra i linguaggi a due o piu' livelli che permette di manipolare sia codice aperto che codice chiuso. Un contributo essenziale per concepire il linguaggio ed il type system e' venuto da una semantica categoriale (non descritta nell'articolo) che generalizza quella proposta in [Mog97]. Precedenti lavori di Pfenning e Davies hanno stabilito delle corrispondenze tra linguaggi multi-livello e logica modale e temporale, sarebbe interessante verificare se tale corrispondenza si estende ad AIM.

[BJM98] e [BJM98b] descrivono Functorial ML e sue estensioni, studiandone sia gli aspetti sintattici che semantici. Sebbene, tali articoli non sono direttamente rilevanti agli obbiettivi del progetto, Functorial ML e' un liguaggio che si presta ad essere analizzato in termini di linguaggi a due livelli (vedi [BM97]), per evidenziare il trattamento a tempo di compilazione delle informazioni sulla struttura dei tipi di dato rappresentati da funtori.

Riferimenti Bibliografici