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]
- 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.. [PS]
- Sketchy introduction to Labelled transition semantics [BP]
- Overview of greatest fixpoints, contextual equivalence and bisimulation [BP2],[JM],[MH]
- Introduction to the PICT language; Core Pict; Programming in PICT; PICT types. [BP],[FB3]
- Subtyping in PICT; Pattern matching; responsive channels. [BP],[FB3]
- Overview of Session Types. [FB7]
- Introduction to the language SePi. [FVM],[FV]
- Programming in SePi. [FVM],[FV]
- Communicating Finite State Machines and some relevant properties [BHvdS], [ET] (Sect.12.1)
- Safety and Liveness properties of systems [ASb], [ASM]
- Overview of Temporal Logic and model cheching [AA], [TB], [MF]
- Explicit-State model-checking algorithm [LD]
- Overview of the Global-Graph coreography model; Projections [ET] (Sect. 9 and 12.2)
- Basics of distributed programming in Erlang and example of calculus for distributed computing: the Ambient Calculus. [STetAl], [LC]
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)
-
[FB] Franco 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]
Franco Barbanera Notes on Data Types in Haskell (html file, last update: 11 Jan 2010)
[B3]
Franco Barbanera Notes on Tail Recursion (html file)
-
[BHivdS]
Franco Barbanera, Rolf Henniker, van der Schoot Systems of Communicating Finite State Machines and related properties (.pdf file)
-
[ET]
Emilio Tuosto A choregraphy-based approach to distributed applications (.pdf 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)
- [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
-
[BP] B.Pierce
Programming in the Pi-Calculus, A Tutorial Introduction to Tamed Pict
(pdf file)(Chapters 1,2.2,2.5.2,3,4,6(only pag.49 and first example of 50))
[BP2] B.Pierce
Foundational Calculi for Programming Languages
(pdf file)(Section 3.3)
- [FB3] F.Barbanera
Summary of [BP] with a few extra notes (file .txt) last update: 6 May 2012.
- [FB7] F.Barbanera
A sketchy overview of Session Types (file .html)
- [FV] J. Franco, V. T. Vasconcelos
Introduction to SePi
- [LC] Luca Cardelli
Introduction to the Ambient Calculus
(pdf file)
- [LD] Laura Dillon
Explicit-State model-checking alogorithm
(pdf file)
- [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:
Optional Reading Material
