Sistema ETD

Archivio digitale delle tesi discusse presso l'Università di Pisa

 

Tesi etd-06072010-152813


Tipo di tesi
Tesi di laurea specialistica
Autore
GALLETTA, LETTERIO
URN
etd-06072010-152813
Titolo
Una semantica astratta per l'inferenza dei tipi ed effetti in un linguaggio multi-tier
Struttura
SCIENZE MATEMATICHE, FISICHE E NATURALI
Corso di studi
INFORMATICA
Commissione
relatore Prof. Levi, Giorgio
Parole chiave
  • analisi statica
  • interpretazione astratta
  • tipi ed effetti
Data inizio appello
16/07/2010;
Consultabilità
parziale
Data di rilascio
16/07/2050
Riassunto analitico
I tipi ed effetti sono una potente estensione dei sistemi di tipo che permettono di esprimere proprietà generali della semantica
dei programmi. I sistemi di tipo e i loro corrispondenti algoritmi di inferenza sono già stati ricostruiti come una gerarchia di
interpretazioni astratte, ma nessuno ha mai considerato il problema di ricostruire l'analisi definita attraverso un sistema di tipi
ed effetti. In questa tesi viene dato un primo contributo in tal senso, ricostruendo un'analisi che permette di dimostrare
proprietà di integrità dei programmi scritti in Links, un linguaggio multi-tier per il web. Usando l'interpretazione astratta
non solo si è ottenuta un'analisi corretta (che è stata implementata in OCaml), ma si è anche dimostrato che l'analisi definita
originariamente per Links non è corretta rispetto alla semantica del linguaggio.
File