Title: Sistemi di tipi calcoli di processi e di sessione
Lecturer: Ilaria Castellani, Rosario Pugliese
Period: October 2015
Place: Università di Firenze, Viale Morgagni
Obiettivo: Il corso mira a presentare alcune tecniche formali, basate su sistemi di tipi, per l'analisi di proprietà di sicurezza in una varieta' di calcoli di processo e di sessione.
Contenuti: Si comincerà con l'introduzione di alcuni sistemi di tipi per la sicurezza per il CCS ed una panoramica di diverse proprietà di sicurezza, con particolare riguardo alla noninterferenza. Si passerà quindi ad approfondire lo studio di sistemi di tipi per calcoli di processi più espressivi del CCS, come il pi-calcolo. Saranno introdotti il "sorting" di Milner e il tipaggio di input/output di Pierce e Sangiorgi, il tipaggio "comportamentale" di Kobayashi, e alcuni sistemi di tipi per la sicurezza del flusso d'informazione. Infine, saranno studiati i calcoli di sessione, che permettono ai processi di organizzare le loro comunicazioni secondo un protocollo predefinito. Saranno presentati alcuni sistemi di tipi per varianti di tali calcoli con sessioni binarie con delega, con sessioni n-arie, con sessioni n-arie con delega e sicurezza, e con sessioni con monitoraggio e adattabilità.