FUNCTIONAL AND CONCURRENT PROGRAMMING PRINCIPLES
Anno accademico 2024/2025 - Docente: Franco BARBANERARisultati di apprendimento attesi
Conoscenza e capacità di comprensione (knowledge and understanding): L'obiettivo del corso e' quello di far entrare in contatto lo studente con alcuni aspetti fondamentali la programmazione funzionale e concorrente sia dal punto di vista teorico che applicativo. Particolare attenzione verra' data, sia che per la programmazione funzionale che per qualla concorrenta, alla teoria dei tipi, intesa come utile strumento per la verifica parziale di correttezza dei programmi.
Capacità di applicare conoscenza e comprensione (applying knowledge and understanding): Lo studioteorico di cui al punto precedente verra' accompagnato alla pratica di programmazione in linguaggi che su tali teorie si basano. Siano essi linguaggi puramente funzionali, come Haskell, oppure linguaggi per la concorrenza per lo sviluppo a livello industriale, come Erlang per al modello ad attori per la concorrenza, oppure linguaggi didattici/sperimentali, come SePi basati sul Pi-calcolo e 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 nel contesto formale del corso le eventuali conoscenze acquisite in passato relativamente alla programmazione funzionale e concorrente.
Abilità comunicative (communication skills):
Capacità di apprendimento (learning skills): Lo studente sara' messo in condizione di poter affrontare autonomamente lo studio di linguaggi funzionali e concorrenti, imparandone a riconoscere ed isolare gli aspetti fondamentali che li caratterizzano
Modalità di svolgimento dell'insegnamento
La prima parte della lezione (circa un terzo della durata complessiva della stessa) viene di solito in parte dedicato allo svolgimento di esercizi (tipicamente piccoli programmi, ma non solo). Il sito del corso contiene un insieme di esercizi, e gli studenti sono invitati ad affrontarli durante lo studio individuale. Quelli in cui gli studenti avessero riscontrato difficolta' vengono affrontati nella prima parte della lezione, su richiesta degli studenti. Sempre nella prima parte il docente invita gli studenti a comunicare eventuali difficolta' incontrate nell'affrontare lo studio degli argomenti delle lezioni precedenti, in modo di poterne cosi' discutere insieme.
Nella seconda parte della lezione si affrontano nuovi argomenti e vengono spesso indicati esercizi relativi agli stessi, tra quelli presenti nella pagina degli esercizi del corso o nuovi (che eventualmente andranno ad incrementare l'insieme degli esercizi disponibili).
Qualora l'insegnamento venisse impartito in modalità mista o a distanza potranno essere introdotte le necessarie variazioni rispetto a quanto dichiarato in precedenza, al fine di rispettare il programma previsto e riportato nel syllabus.
Prerequisiti richiesti
Nozioni base di Logica Matematica, Modelli Computazionali, Teoria degli automi e dei Linguaggi Formali.
Frequenza lezioni
La frequenza e' obbligatoria.
Contenuti del corso
Il corso di Functional and Concurrent Programming Principles fornisce una solida base per i paradigmi di programmazione funzionale e concorrente, esplorando concetti teorici e pratici attraverso linguaggi avanzati e modelli computazionali.
Il corso inizia con un'introduzione alla programmazione funzionale, dove vengono presentati i concetti principali di questo paradigma. Gli studenti impareranno le basi della programmazione in Haskell, uno dei linguaggi di programmazione funzionale più utilizzati, con particolare attenzione alla teoria dei tipi semplici e alla sua applicazione nel linguaggio, utile per garantire la correttezza e la sicurezza del codice.
La seconda parte del corso introduce la programmazione concorrente, concentrandosi sui concetti di base e i modelli utilizzati in questo ambito. Viene approfondito il modello degli attori, un paradigma che consente la comunicazione tra processi concorrenti senza condividere lo stato. Gli studenti esploreranno la programmazione concorrente nei linguaggi non-imperativi, con un focus su Erlang, un linguaggio funzionale progettato per supportare la concorrenza su larga scala.
Il corso introduce inoltre il Pi-calculus, un modello computazionale per la computazione concorrente via message-passing, con mobilita'. Tale modello verra' utilizzato come base per la comprensione della teoria dei tipi sessione. Si esaminano linguaggi sperimentali come SePi, che combinano Pi-calculus e tipi sessione per gestire la concorrenza in modo più sicuro e strutturato. A ciò si affianca l'introduzione alle coreografie e ai tipi di sessione multiparty, che modellano la comunicazione tra più processi in un sistema concorrente.
Il corso include una trattazione del teorema del punto fisso, fondamentale per la logica e i sistemi concorrenti, e una panoramica sulla logica temporale e il model checking, tecniche utilizzate per verificare formalmente le proprietà di sistemi concorrenti. Infine, viene fornita una panoramica sui calcoli degli ambienti e sulle reti di Petri, modelli utili per descrivere e analizzare sistemi distribuiti e concorrenti.
Testi di riferimento
Programmazione del corso
| Argomenti | Riferimenti testi | |
|---|---|---|
| 1 | Introduzione alla Progr. Funzionale | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
| 2 | Introduzione ad Haskell e tipi in Haskell.Overview del lambda-calcolo. | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
| 3 | Teoria dei tipi semplici ed applicazioni ad Haskell | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
| 4 | Il modello di programmazione concorrente ad attori. | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
| 5 | Programmazione in Erlang | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
| 6 | Introduzione al pi-calcolo. | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
| 7 | Introduzione ai Session Types. | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
| 8 | Introduzione a SePi | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
| 9 | Programmazione in SePi. | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
| 10 | Il meccanismo della delegation nei session types. Esempi in SePi. | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
| 11 | Coreographies: Gglobal protocols, local protocols. | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
| 12 | Multiparty session types. | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
| 13 | Logica temporale e Model Checking | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
| 14 | Ambient calculus e Reti di Petri | https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html |
Verifica dell'apprendimento
Modalità di verifica dell'apprendimento
Nella prova scritta verranno proposti quesiti relativi alla parte teorica del corso; verra' altresi' richiesto di sviluppare piccoli programmi nei linguaggi di programmazione affrontati nel corso.
La verifica dell’apprendimento potrà essere effettuata anche per via telematica, qualora le condizioni lo dovessero richiedere.
Gli studenti con disabilità e/o DSA dovranno contattare con sufficiente anticipo rispetto alla data dell'esame il docente, il referente CInAP del DMI (prof.ssa Daniele) e il CInAP per comunicare che intendono sostenere l'esame fruendo delle opportune misure compensative.