FUNCTIONAL AND CONCURRENT PROGRAMMING PRINCIPLES

Academic Year 2024/2025 - Teacher: Franco BARBANERA

Expected Learning Outcomes

Knowledge and understanding: The course aims  to make the students aquainted with some of the fundamental aspects of functional and concurrent programming.  Students will learn to recognize the "core" and relevant parts common to all functional and concurrent  programming languages, as well as to isolate their characterizing parts, As a relevant tool for the formal partial verification of programs, Type Theory will play a relevant role in the course.

Applying knowledge and understanding: The study of  foundational aspects will be paired with programming activities on different actual languages, such as Haskell for funcltional programming and  Erlang (based on the actor concurrency model) for functional/concurrent programming. Didactic/sperimental languages will also be dealt with in order to actually apply principles of Session Types.

Making judgements: The students will be encouraged to autonomously applying - on simple but actual programming examples - what learned in the general context of the foundational theories. They will be also encouraged to frame their past functional/concurrent programming experiences in the more formal part of the course..

Communication skills: The students will acquire the necessary communication skills and expressive ability in order to express in a formal and non-ambiguous way topics and  arguments related to distributed and concurrent programming.

Learning skills: The students will be anabled to autonomously facing the study of functional and concurrent languages, as well as to recognize and isolate their characterizing foundational aspects.

Course Structure

The course site contains a remarkable set of exercises, and students are invited to tackle them during self-study. 
Those in which the students encountered difficulties are addressed in the first part of the lesson, at the students' request.
Also in the first part, the teacher invites the students to communicate any difficulties encountered in tackling the study of the topics
of the previous lessons, so that we can discuss them together. In the second part of the lesson, new topics are addressed and exercises relating to them are often indicated, among those present on the course
exercises page or new ones (which will eventually increase the set of available exercises). As in the previous year, we will try to organize numerous ongoing tests, the evaluation of which will allow you to be exempted from taking part of the final exam.

Should teaching be carried out in mixed mode or remotely, it may be necessary to introduce changes with respect to previous statements, in line with the programme planned and outlined in the syllabus.

Learning assessment may also be carried out on line, should the conditions require it.

Required Prerequisites

Base notions of Mathematical Logic, Computational Models, Formal Languages and Automata Theory. 

Attendance of Lessons

Attendance is compulsory.

Detailed Course Content

The Functional and Concurrent Programming Principles course provides a solid foundation for 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, where the main concepts of this paradigm are presented. Students will learn to program in Haskell, one of the most widely used functional programming languages, with a focus on the simple theory of types and its application in the language, useful for ensuring the correctness and safety of code. The second part of the course introduces concurrent programming, focusing on the basic concepts and models used in this field. The actor model is explored in depth, a paradigm that allows communication between concurrent processes without sharing state. 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 Pi-calculus, a computational model for concurrent computation via message-passing, with mobility. This model will be used as a basis for understanding session type theory. Experimental languages ​​such as SePi, which combine Pi-calculus and session types to handle concurrency in a safer and more structured way, are examined. This is accompanied by an introduction to choreographies and multiparty session types, which model communication between multiple processes in a concurrent system. The course includes a discussion of the fixed-point theorem, which is fundamental to logic and concurrent systems, and an overview of temporal logic and model checking, techniques used to formally verify the properties of concurrent systems. Finally, an overview of room calculi and Petri nets, useful models for describing and analyzing distributed and concurrent systems, is provided.

Textbook Information

Course Planning

 SubjectsText References
1Introduction to Functional programminghttps://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html
2Introduction to Haskell and types in Haskell.Overview of lambda-calculus.https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html
3Theory of simple types and ita application to Haskellhttps://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html
4The Actor model of cuncurrent programming https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html
5Programming in Erlanghttps://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html
6Introduction to pi-calcolo. https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html
7Introduction to Session Types.https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html
8Introduzione a SePihttps://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html
9Programming in SePi. https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html
10The delegation mechanism in  . SePi examples.https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html
11Coreographies: global protocols, local protocols.https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html
12Multiparty session types.https://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html
13Temporal Logic and Model Checkinghttps://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html
14Ambient Calculus and Petri netshttps://www.dmi.unict.it/barba/PRINC-FUN-CONC/PROGRAMMI-TESTI/index.html

Learning Assessment

Learning Assessment Procedures

In the written test, questions relating to the theoretical part of the course will be asked; the student will also be asked to develop small programs in the programming languages ​​covered in the course.

Verification of learning can also be carried out electronically, should conditions require it.

Students with disabilities and/or DSA must contact the teacher, the CInAP contact person of the DMI (Prof. Daniele) and the CInAP sufficiently in advance of the exam date to communicate that they intend to take the exam taking advantage of the appropriate compensatory measures.

Examples of frequently asked questions and / or exercises

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