Linguaggi per il Global Computing

Laurea Magistrale in Informatica - Università di Padova
Anno Accademico 2020/2021

Obiettivi del corso

L'enorme diffusione dei sistemi concorrenti, distribuiti e mobili rende inadeguati i paradigmi di specifica e programmazione classici ed apre sfide complesse e affascinanti. Appare necessario un ripensamento, che parta dalle stesse fondamenta e che adotti un approccio rigoroso, formale, disciplinato. Il corso si propone di avvicinare lo studente a tematiche di interesse in questo ambito. Parte dai fondamenti oramai classici dei linguaggi concorrenti, che pongono al centro dello studio i concetti di processo, le metodologie di composizione, i meccanismi di comunicazione (come il Calculus of Communicating Systems ed il Pi-Calculus) per poi illustrare le ricadute sui linguaggi per la concorrenza e la distribuzione quali ad esempio Google Go, Erlang, Elixir, Clojure, Jolie, Rust, e le corrispondenti tecniche di programmazione. Il corso dà luogo al conseguimento di 6 CFU.

Programma di massima del corso

Il corso, della durata di 48 ore, svilupperà i seguenti temi:
  1. Il "calculus of communicating systems" (CCS), un linguaggio minimale per la descrizione di sistemi concorrenti. Equivalenza di processi: Sistemi di transizione e bisimulazione
  2. Logica di Hennessy-Milner e strumenti per la verifica. Mutua esclusione, deadlock, fairness. Proprietà di safety e liveness. Sistemi con topologia dinamica e mobilità: pi-calcolo. Strumenti di verifica (Concurrency Workbench, Caal, PseuCo).
  3. Dai linguaggi di specifica ai linguaggi di programmazione: Google Go, Erlang, Elixir, Clojure, Rust, Jolie, ORC.

Orario del corso

Il corso fa parte del Corso di Laurea Magistrale in Informatica, Università di Padova, ed è collocato nel II semestre dell'Anno Accademico 2020/2021 , con il seguente orario (se necessario modifiche all'orario potranno poi essere valutate con i partecipanti al corso). Le lezioni si svolgeranno in modo duale (in presenza e trasmesse a distanza via Zoom).
Giorno Orario Aula
Lunedì 14.30 - 16.00 2BC/60
Martedì 14.30 - 16.00 2BC/60

Modalità d'Esame e Appelli

L'esame si compone di due parti: esercizi ed approfondimento/progetto (vedi sotto), da preparare off-line e poi presentare in forma orale/seminariale.

  1. ESERCIZI
    Dovreste svolgere due esercizi nella sezione Esercizi di questa pagina
  2. APPROFONDIMENTO/PROGETTO
    Potete scegliere tra varie possibilità che comprendono un mini-progetto di specifica/implementazione/verifica formale di proprietà oppure lo studio di tool di verifica sofisticati oppure un approfondimento su tematiche relative a modelli formali, tecniche di verifica, linguaggi di programmazione in qualche modo connessi ai temi del corso. Anche in questo caso, alcuni suggerimenti si trovano nella pagina dell'esame.
In entrambi i casi, le liste di suggerimenti non sono esaustive. E' possibile proporre temi di approfondimento differenti che rispondano ad interessi personali (anche esercizi diversi, ad esempio scelti dal libro). Una volta effettuata la scelta, si consiglia di contattare il docente per la definizione dei dettagli (esercizi e approfondimenti sono spesso descritti in modo sommario).

Riferimenti bibliografici e materiale didattico

Il corso ha un Moodle che verrà utilizzato per comunicazione e distribuzione di parte del materiale. Per la parte fondazionale si utilizzerà il seguente libro

Il materiale relativo ai linguaggi di programmazione discussi a lezione è fornito tramite il moodle.

Link Utili per fini didattici

Alcuni strumenti avanzati