Title: Introduction to process calculi and related type systems

Lecturer: Ilaria Castellani, Rosario Pugliese

Period: 1, 2, 3, 9, 10, 11, 14, 15, 16, 17 december 2015, 14.30 -- 16.30 

Place: Università di Firenze, Viale Morgagni, Aula Anfiteatro

This course aims at introducing, and motivating the use of, some basic formal methods from Concurrency Theory. It is split in two parts. Firstly, some well-known process calculi, e.g. CCS and pi-calculus, are presented together with the most commonly used techniques for defining their operational and observational semantics. Then, many type systems are presented for ensuring different properties of distributed and concurrent processes, such as e.g. correctness of interaction and security.

Lectures & topics:

1. CCS: syntax and operational semantics. Observational semantics. Trace equivalence.

2. Strong & weak bisimilarity. Axiomatic alternative characterisation. Reduction semantics & barbed bisimilarity. Coincidence result. Link mobility. Introduction to pi-calculus.

3. Pi-calculus: syntax and operational semantics. Reduction semantics. Polyadic variant and its encoding. Data encoding: boolean values and operators.

4. Early & late operational semantics. Observational semantics: late bisimilarity, early bisimilarity, barbed congruence. Coincidence result.

5. Introduction to type systems for the pi-calculus: Milner's sorting & I/O typing by Pierce and Sangiorgi.

6. An advanced type system: Kobayashi's usage types.

7. Binary session calculi and associated type systems.

8. Multiparty session calculi and associated type systems.

9. Type systems for security: the linear pi-calculus & enhanced session types.

10. Session calculi with monitoring and adaptation.