Tipo di tesi
Tesi di laurea specialistica
Titolo
Una semantica astratta per l'inferenza dei tipi ed effetti in un linguaggio multi-tier
Dipartimento
SCIENZE MATEMATICHE, FISICHE E NATURALI
Corso di studi
INFORMATICA
Riassunto (Italiano)
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.
