• analisi statica
• interpretazione astratta
• tipi ed effetti

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.