The list of the arguments of the course, together with the material to study.

Concurrent and distributed programming in non-imperative programming paradigms. Introduction to Functional Programming. [FB].1-5, [FBb]
Main functional-programming concepts: Order of evaluation, Recursion; Higher-order functions; Anonymous functions; Curryfication; Lists; Recursion; Tail recursion; Correctness proofs. [FB].6-12, [B3]
Introduction to Haskell; Polymorphic types; Pattern Matching; Type Classes. Infinite structures. [HPF],[B2]
Infinite structures in Haskell; Introduction to Monads and I/O in Haskell. [HPF] ,[JN]
Introduction and Short review of the λ-calculus: λ-terms, free and bound variables, α-conversion, substitution; theory of β-reduction and some fundamental results; overview of the theory of β-conversion. [FBb], [FB].13
Types for functional programming; The Curry approach to types; Type assignement; Principal Pair algorithm [FB].14
The actors model of concurrent programming; Sequential programming in Erlang [AS],[FB5],[JAetal](For the sequential part of Erlang it is enough the Hands-on tutorial whose link is in the Interpreters and manuals section below.)
Concurrent Programming in Erlang [JAetal],[FB5]
Program examples in Erlang [AAVV]
Process calculi: Introduction to the Pi-calculus; Structural congruence; Scope extrusion; reduction semantics; Sketchy introduction to Labelled transition semantics [PS]
Knaster-Tarski theorem and bisimulation [JM],[MH]
Overview of Session Types. [FB7]
Introduction to the language SePi. [FVM],[FV]
Programming in SePi. [FVM],[FV]
Introduction to Multiparty Sessions [BdL]
Safety and Liveness properties of systems [ASb], [ASM]
Overview of Temporal Logic and model cheching [AA], [TB], [MF]
Explicit-State model-checking algorithm [LD]
Basics of distributed programming in Erlang [DetAl]

Reading Material

[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 (no pp algorithm, no unify algorithm) (html file, last update: March 2016)
[FBb] F.Barbanera Computazioni, Programmazione funzionale e Preludio al lambda-calcolo (file .pdf, updated 14 Dic 2018) (LaTeX source)
[B2] F.Barbanera Notes on Data Types in Haskell (html file, last update: 11 Jan 2010)
[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 (link to external html file, a version also in here )(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 alogorithm
[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)
[D-EtAl] AA.VV. A pi-calculus with multiparty session types (pdf file) Sections 1 and 2.
[D-EtAl] Simon Thompson et Al., Erlang Programming. (Book) Published by O'Reilly Media. Chapter 11, up to section "Node Connections" (excluded)

Interpreters, Compilers and Manuals:

Interpreters and Manuals for Haskell can be found in The Haskell Homepage
Interpreters and Manuals for Scheme can be downloaded from Schemers.org. A good interpreter for Scheme can be downloaded from PLT scheme Homepage
The Pict compiler is available in a on-line version on the site The On-line Pict Compiler (by Claudio Marino; Thanks to Gerardo Maiorano).
The Pict compiler can be also downloaded from The Pict Compiler (it is a working version, with graphic interface (by Fulvio Brancato), of the compiler that can be found in The Pict Homepage.)
An on-line version of SePi can be found in SePi by example
An Eclipse SePi plug-in can be found in Eclipse SePi plug-in
An on-line version of Scribble
The Scribble Site
Compiler and manual for Erlang can be found in Erlang home
A hands-on (simulator) for Erlang can be found in Hands-on tutorial for Erlang
It is possible to program and complile on-line with several programming languages on this Codinggroung site (thanks to Alessandro Ortis).

Optional Reading Material

Dexter Kozen and Alexandra Silva Practical Coinduction (.pdf file)
The Benchmark Game
Functional Programming in the real world
Francesco Cesarini, Simon Thompson; Erlang Programming A Concurrent Approach to Software Development
Kazimierz Trzęsicki TEMPORAL LOGIC MODEL CHECKERS AS APPLIED IN COMPUTER SCIENCE* (.pdf file)

SYLLABUS and READING MATERIAL

Syllabus and tentative schedule

Reading Material