FUNCTIONAL AND CONCURRENT PROGRAMMING PRINCIPLES

The Functional and Concurrent Programming Principles course provides a solid foundation in functional and concurrent programming paradigms, exploring theoretical and practical concepts through advanced languages ​​and computational models. The course begins with an introduction to functional programming, presenting the main concepts of this paradigm. Students will learn the basics of programming in Haskell, one of the most widely used functional programming languages, with a focus on simple type theory and its application to the language, which is useful for ensuring code correctness and security. Concurrent programming will then be introduced, focusing on the basic concepts and models used in this field. The actor model, a paradigm that allows communication between concurrent processes without sharing state, will be explored in depth. Students will explore concurrent programming in non-imperative languages, with a focus on Erlang, a functional language designed to support large-scale concurrency. The course also introduces the Pi-calculus, a computational model for concurrent computation via message-passing, with mobility. This model will be used as a foundation for understanding session type theory. Experimental languages ​​such as SePi, which combine Pi-calculus and session types to manage concurrency in a safer and more structured way, will be examined. This is complemented by an introduction to choreographies and multiparty session types, which model communication between multiple processes in a concurrent system. During the discussion of multiparty session types, we will briefly discuss the trace semantics of concurrent systems and the notions of coinduction and bisimulation. The course includes a discussion of the fixed-point theorem, fundamental for defining notions relevant to concurrent systems, and an overview of temporal logic and model checking, techniques used to formally verify the properties of concurrent systems. Abstract definitions of safety and liveness properties for concurrent systems will also be explored.

All reference texts for the course are available and downloadable in electronic format from the page

 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)

The exam consists of a written test. The written test will include questions related to the theoretical part of the course; students will also be asked to develop small programs in the programming languages ​​covered in the course. Part of the written test may be replaced by small projects proposed during the course. This possibility, however, is dependent on the number of students attending. These tests may be conducted online, if conditions require. The oral exam may be held on the same day as the written test or a few days after it. The following criteria will generally be used to assign the final grade:

 - Not passed: The student has not mastered the basic concepts and is unable to complete the exercises. 

- 18-23: The student demonstrates minimal mastery of the basic concepts, their ability to present and connect content is modest, and they can solve simple exercises.

 - 24-27: The student demonstrates a good command of the course content, good presentation and connection skills, and completes the exercises with few errors. 

- 28-30 with honors: The student has mastered all the course content and is able to present it thoroughly and connect it critically; he or she completes the exercises completely and error-free.

 Students with disabilities and/or learning disabilities (LD) must contact the instructor, the DMI CInAP representative (Prof. Daniele), and CInAP well in advance of the exam date to communicate their intention to take the exam with appropriate compensatory measures.

The webpage 

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

contains exercises related to the topics covered in the course. These exercises are representative of the types of questions asked in the written exam. Please note that these questions are purely indicative: the actual questions asked in the exam may differ, even significantly, from those listed here. 

During lectures, exercises similar to those students will complete in their final exam will be completed. Additional exercises will be made available during lectures.