Un sistema di tipi per l'analisi del deadlock in programmi funzionali, concorrenti e comunicanti.

Negli ultimi anni sono stati definiti vari sistemi di tipo per assicurare proprietà di correttezza di programmi concorrenti basati sulla comunicazione. Tra queste priorietà figura l'assenza di deadlock, ovvero di stati irreversibili in cui la computazione non può proseguire a causa di dipendenze circolari tra canali di comunicazione. Tutti i sistemi di tipo definiti, tuttavia, fanno riferimento a calcoli di processi che, per quanto espressivi, non rappresentano fedelmente la struttura di programmi convenzionali, nei quali si fa ampio uso di astrazioni quali procedure e funzioni. Lo scopo della tesi è la definizione di un sistema di tipi per assicurare l'assenza di deadlock in programmi scritti in un linguaggio funzionale che include primitive per la concorrenza e la comunicazione su canali lineari (in pratica, il nucleo di Concurrent ML). La scelta di focalizzarsi su canali lineari, ovvero canali sui quali è possibile effettuare una sola comunicazione, è motivata da diversi fattori. In primo luogo, molti canali usati comunemente in sistemi concorrenti sono lineari. In secondo luogo, comunicazioni strutturate più complesse, che coinvolgono lo scambio di svariati messaggi, possono essere codificate in termini di comunicazioni lineari grazie alla possibilità di inviare canali come messaggi. Infine, i programmi che comunicano su canali lineari sono confluenti ed il sistema di tipi può trarre vantaggio dalla linearità per gestire configurazioni di processi che, seppur comuni nella pratica, sfuggono alle tecniche di analisi statica attualmente disponibili. La tesi comprende la definizione di sintassi e semantica del linguaggio preso come riferimento, la definizione del sistema di tipi, nonché la dimostrazione formale delle proprietà dei programmi ben tipati.