FONDAMENTI E LINGUAGGI PER LA PROGRAMMAZIONE DISTRIBUITA
Anno accademico 2017/2018 - 1° anno - Curriculum Sistemi di Rete e SicurezzaCrediti: 6
Organizzazione didattica: 150 ore d'impegno totale, 102 di studio individuale, 24 di lezione frontale, 24 di esercitazione
Semestre: 2°
Obiettivi formativi
Conoscenza e capacità di comprensione (knowledge and understanding): L'obiettivo del corso e' quello di far entrare in contatto lo studente con alcune teorie fondazionali per la programmazione concorrente e distribuita. Lo studente imparera' quindi a riconoscere quello che accomuna la gran parte dei linguaggi concorrenti e distribuiti, ed a isolarne gli aspetti che invece li caratterizzano.
Capacità di applicare conoscenza e comprensione (applying knowledge and understanding):: Lo studio di molte delle teorie fondazionali di cui al punto precedente verra' accompagnato alla pratica di programmazione in linguaggi che su tali teorie si basano. Siano essi linguaggi per lo sviluppo a livello industriale, come Erlang per al modello ad attori per la concorrenza, sieno essi linguaggi didattici o sperimentali, come PICT per quanto riguarda la teoria del pi-calcolo o SePi per la Teoria dei Session Types.
Autonomia di giudizio (making judgements): Lo studente verra' stimolato a cercare di applicare autonomamente quanto imparato nel contesto fromale delle teorie fondazionali presentate ad esempi didattici, ma concreti di programmazione. Verra' inoltre stimolato a inquadrare le eventuali conoscenze acquisite in passato relative alla programmazione concorrente e distribuita nel contesto astratto delle teorie fondazionali affrontate nel corso.
Abilità comunicative (communication skills):
Capacità di apprendimento (learning skills): Lo studente sara' messo in condizione di poter affrontare autonomamente lo studio di linguaggi concorrenti e distribuiti, imparandone a riconoscere ed isolare gli aspetti fondamentali che li caratterizzano
Conoscenza di base delle basi teoriche della programazione concorrente e distribuita.
Capacita' di comprensione del significato degli aspetti teorici della programmazione concorrente e distribuita.
Capacita' di utilizzare nozioni teoriche nella comune pratica di programmazione concorrente e distribuita.
Capacita' di valutare, giudicare ed utilizzare linguaggi, metodologie e tecniche per la programmazione concorrente e distribuita nel contesto piu' generale ed astratto delle teorie fondazionali.
Prerequisiti richiesti
Elementi di base di logica; elementi di base di programmazione concorrente.
Frequenza lezioni
Non obbligatoria.
Contenuti del corso
- Concurrent and distributed programming in non-imperative programming paradigms. Introduction to Functional Programming.
- Main functional-programming concepts: Order of evaluation, Recursion; Higher-order functions; Anonymous functions; Curryfication; Lists; Recursion; Correctness proofs.
- Short review of the Lambda-calculus
- Types for functional programming.
- Introduction to Haskell; Polymorphic types; Pattern Matching; Type Classes. Infinite structures.
- Tail recursion
- The actors model of concurrent programming; A Concurrent functional language: Erlang
- Concurrent Programming in Erlang
- Process calculi: Introduction to the Pi-calculus;.
- Process calculi: Sketchy introduction to contextual equivalence and bisimulation
- Introduction to the PICT language; Core Pict.
- Overview of Session Types.
- Session and Refinement Types: the language SePi.
- Introduction to Scribble
- An experimental language with multiparty session types
- Overview of process calculi for distributed programming.
- Basics of distributed programming in Erlang.
Testi di riferimento
http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html
Programmazione del corso
Argomenti | Riferimenti testi | |
---|---|---|
1 | Introduzione alla Progr. Funzionale | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
2 | Introduzione ad Haskell e tipi in Haskell. Introduzione al lambda-calcolo. | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
3 | Lambda Calcolo: i termini, Variabili libere e legate, sostituzione. Teoria della beta-riduzione e risultati fondamentali. Cenni di teoria della beta-conversione. | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
4 | Il modello di programmazione concorrente ad attori. Introduzione ad Erlang. | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
5 | Programmazione in Erlang | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
6 | Introduzione al pi-calcolo. Processi, scope-extrusion. | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
7 | Semantica operazionale del pi-calcolo. Cenni di transizioni etichettate. Introduzione a PICT. | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
8 | Tipi in PICT. Programmazione PICT. | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
9 | Subtyping in PICT | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
10 | Pattern matching: definizione e implementazione | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
11 | Responsive channels. Programmazione in PICT. | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
12 | Cenni sul Type Checker di PICT | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
13 | Introduzione ai Session Types. | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
14 | Introduzione a SePi | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
15 | Programmazione SePi. Cenni di Equivalenza contestuale e bisimulation. | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
16 | Il meccanismo della delegation nei session types. Esempi in SePi. | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
17 | Refinement Types. Assume and Assert in SePi | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
18 | Introduction to Scribble: Global protocols, local protocols, projections and comunicating finite state automata. | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
19 | Multiparty session types: overview. | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
20 | A pi-calculus with multiparty session types | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
21 | Distributed pi-calculi. Programmazione distribuita in Erlang: costrutti principali. | http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/PROGRAMMI-TESTI/programmaAAcorrente.html |
Verifica dell'apprendimento
Modalità di verifica dell'apprendimento
Scritto e orale.
Esempi di domande e/o esercizi frequenti
http://www.dmi.unict.it/~barba/FOND-LING-PROG-DISTR/ESERCIZI/index.html