FUNCTIONAL AND CONCURRENT PROGRAMMING PRINCIPLES

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 studio teorico 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 ad applicare autonomamente ad esempi didattici, ma concreti di programmazione quanto imparato nel contesto formale delle teorie fondazionali presentate nel corso. 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):  -

Le abilità comunicative  acquisite riguardano la capacità di spiegare in modo chiaro e corretto concetti, definizioni e dimostrazioni, usando il linguaggio adatto. In altre parole, lo studente sapra’ argomentare con logica, farsi comprendere anche da chi non è esperto e discutere problemi teorici in modo ordinato e preciso.

Capacità di apprendimento (learning skills):

L’insegnamento si svolge attraverso lezioni frontali e attività di laboratorio/esercitazione. Le lezioni introdurranno i concetti teorici, mentre il laboratorio ne permetterà l’applicazione pratica tramite esercitazioni e casi studio.

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.

Nozioni base di Logica Matematica, Modelli Computazionali, Teoria degli automi e dei Linguaggi Formali. Elementi di base di programmazione concorrente.

Per una comprensione approfondita degli argomenti trattati e delle metodologie presentate, si raccomanda vivamente la regolare partecipazione alle lezioni.

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.

Verra’ poi introdotta 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. Durante la trattazione dei tipi sessione multiparty si prendera’ spunto per discutere brevemente della semantica a tracce dei sistemi concorrenti e delle nozioni di coinduzione e bisimulazione.

Il corso include una trattazione del teorema del punto fisso, fondamentale per la definizione di nozioni rilevanti per i sistemi concorrenti, e una panoramica sulla logica temporale e il model checking, tecniche utilizzate per verificare formalmente le proprietà di sistemi concorrenti. Saranno anche affrontate le definizioni astratte di proprieta’ di safety e di liveness per sistemi concorrenti.

I testi di riferimento per il corso sono tutti reperibili e scaricabili in formato elettronico dalla pagina

https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html

• [AA] A.Artale Slides on Linear Temporal Logic (pdf file) (slides 1-17 and 24-44)
• [ASb] B.Alpern, F.B.Schneider Defining Liveness (pdf file) (fino a Uniform Liveness esclusa, piu' enunciato Theorem 1)
• [ASM] B.Alpern, F.B.Schneider, J.Melnyk Defining Liveness (slides) (pdf file) (fino a Uniform Liveness esclusa, piu' enunciato Theorem 1)
• [BdL] F.Barbanera, Ugo de'Liguoro A Simple Introduction To Multiparty Sessions (pdf file)
• [FB] F.Barbanera Short Introduction to Functional Programming and the Lambda-Calculus
• [FBb] F.Barbanera Computazioni, Programmazione funzionale e Preludio al lambda-calcolo (file .pdf, updated 14 Dic 2018)
• [B2] F.Barbanera Notes on Data Types in Haskell  (html file)
• [B3] F.Barbanera Notes on Tail Recursion  (html file)
• [HPF] P.Hudak, J.Peterson, J.H.Fasel A Gentle Introduction to Haskell 98  (pdf file) (To be studied: Ch.s 1-3; Ch. 4: only pag.15; Ch.5: only up to the first half of page 25; Ch.7: up to page 33 included)
• [JN]Jeff NewbernAll About Monads )(downlodable .zip version) (Overview, Intro to Maybe and IO).
• [AS]A.Shali Actor Programming in Chapel (.pdf file; Section 2(no 2.5))
• [FB5] F.Barbanera Short Notes On Erlang and Actors (.html file) last update: 18 June 2012
• [JAetal1]J.Armstrong et al. Concurrent Programming in Erlang (.pdf file; 5.1-5.4)
• [JM] Jayadev Misra KnasterTarski Theorem (.pdf file; Fino ad enunciato del teorema incluso.)
• [MH] Matthew Hennessy Bisimulation as fixed point (.pdf file)
• [AAVV] Erlang Examples (.txt file;)
• [PS] P.Sewell Applied Pi, A brief tutorial (pdf file) Chapters 1(except 1.5), 2
• [FB7] F.Barbanera A sketchy overview of Session Types (file .html)
• [FV] J. Franco, V. T. Vasconcelos Introduction to SePi
• [LD] Laura Dillon Explicit-State model-checking algorithm
• [FVM] J. Franco, V. T. Vasconcelos, D. Mostrous SePi by Example
• [MF] M.Franceschet Slides on Model Checking (pdf file) (slides 4-28 and 44-63)
• [TB] T.Bultan Slides on Computational-Tree Temporal Logic (pdf file) (slides 2-5)

L'esame consiste in una prova scritta.  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. Parte della prova scritta potra’ essere sostituita dallo svolgimento di piccoli progettini proposti durante lo svolgimento del corso. Tale possibilita’ e’ comunque da ritenersi dipendente dalla numerosita’ degli studenti frequentanti.

Tali prove potranno avere luogo per via telematica, qualora le condizioni lo dovessero richiedere. La prova orale potrà svolgersi il giorno stesso in cui è stata svolta la prova scritta o a distanza di pochi giorni da esso.

Per l'attribuzione del voto finale si seguiranno di norma i seguenti criteri:
- non approvato: lo studente non ha acquisito i concetti di base e non è in grado di svolgere gli esercizi.
- 18-23: lo studente dimostra una padronanza minima dei concetti di base, le sue capacità di esposizione e di collegamento dei contenuti sono modeste, riesce a risolvere semplici esercizi.
- 24-27:  lo studente dimostra una buona padronanza dei contenuti del corso, le sue capacità di esposizione e di collegamento dei contenuti sono buone,  risolve gli esercizi con pochi errori.
- 28-30 e lode: lo studente ha acquisito tutti i contenuti del corso ed è in grado di esporli compiutamente e di collegarli con spirito critico; risolve gli esercizi in modo completo e senza errori.

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.

Nella pagina web

https://www.dmi.unict.it/barba/PRINC-FUN-CONC/ESERCIZI/index.html

sono presenti esercizi relativi agli argomenti trattati nel corso. Tali esercizi sono rappresentativi del tipo di domande proposte nell'esame scritto.

Si precisa che tali domande hanno carattere puramente indicativo: le domande effettivamente proposte in sede d’esame potranno divergere, anche in modo significativo, da quelle riportate in questa lista.

Durante le lezioni verranno svolti degli esercizi simili a quelli che gli studenti dovranno affrontare nel loro esame finale. Ulteriori esercizi verranno resi disponibili nel corso delle lezioni.