Un calcolo formale per gli attori Scala Akka e i loro tipi

Scopo di questa tesi è presentare un calcolo formale che modelli il comporta-mento degli attori Scala Akka. In particolare in questo lavoro viene presentatoun linguaggio A che modella la creazione degli attori, lo scambio di messaggi eil cambio di comportamento. All’interno dell’elaborato viene data evidenza dicome l’esecuzione dei programmi scritti in A e in Akka coincida. Viene poi dataun’estensione del linguaggio A in modo da inserire la gerarchia degli attori e laterminazione. Anche le esecuzioni dei programmi scritti nel nuovo linguaggioesteso A+ mostrano essere le stesse dei corrispondenti programmi scritti in Ak-ka. Infine viene presentato un sistema di tipi per il linguaggio A che si ispiraal modulo sperimentale Akka Typed e viene dimostrato che se un programmascritto nel nostro linguaggio formale è ben tipato, allora si può garantire che, atempo di esecuzione, ogni attore sarà in grado di gestire tutti i messaggi che glivengono inviati.