La logica è senza dubbio una delle discipline che più hanno contribuito alla nascita dell'informatica. Ma oggi, ai tempi dei laptop piccoli e superveloci e delle reti sociali, questa paternità è ancora riconoscibile? Nel seminario verrà presentato un aspetto dell'informatica che utilizza pienamente concetti e tecniche logiche per il proprio sviluppo - e che per certi aspetti si identifica con la logica stessa - quello dello studio dei modelli di calcolo formali. Questi sono indispensabili per una comprensione approfondita dei sistemi di calcolo e per dimostrarne le proprietà desiderate. In particolare l'attenzione si concentrerà sulla programmazione con vincoli (di cui la programmazione logica è un caso particolare) e sui calcoli di processo. Questi sono dotati tra l'altro di una semantica astratta e di una logica adeguata, cioè due processi non sono equivalenti se e solo se esiste almeno una proprietà esprimibile nella logica che è posseduta da uno ma non dall'altro processo.
|