Thursdays, 10-12
Room: 3A18
Starting 8th February

PhD course, 2.5 ECTS
Exam: paper presentation in the second part of the course

Contact: Agata Murawska (agmu@itu.dk)
We also have a mailing list, concurrency-theory@itu.dk, which can be joined here

Unless stated otherwise, presentations are given by Marco Carbone

Feb. 8 Calculus of Communicating Systems
Syntax, semantics, limitations
Based on: R. Milner, "Communication and Concurrency"

Feb. 15 Calculus of Communicating Systems
Reduction semantics, trace equivalence, bisimulation and bisimilarity, weak bisimulation and weak bisimilarity
Based on: R. Milner, "Communication and Concurrency"

Feb. 22 Pi Calculus
Based on: J. Parrow, "An introduction to the pi-calculus" (available online)

Mar. 1 True concurrency
Speakers: Thomas Hildebrandt and Håkon Normann
Based on:
M. Mukund, M. Nielsen, "CCS, locations and asynchronous transition systems" (available online. skip pages 20-30)
T. Hildebrandt, Ch. Johansen, H. Normann, "A Stable Non-interleaving Early Operational Semantics for the Pi-calculus" (available here)

Mar. 8 Guest talk: Reversible Event Structures
Speakers: Eva Graversen and Nobuko Yoshida
Imperial College London http://mrg.doc.ic.ac.uk/

Abstract
We first talk about a summary of recent activities in Mobility Session Type Group in Imperial College London. Then we talk about the main technical topic.

Event structures have been used for modelling forward-only process calculi. We define (categories of) reversible variants of prime, asymmetric, bundle, extended bundle, and general event structures for the purpose of using one of these variants to define truly concurrent semantics of reversible process calculi. We use the causal subcategory of reversible bundle event structures to define semantics of, CCSK, a reversible variant of CCS. We also expand CCSK to control the reversibility using a rollback primitive, which reverses a specific action and all actions caused by it. To define the event structure semantics of rollback, we use extended bundle event structures, which add asymmetric conflict to bundle event structures, and use their capacity for non-causal reversibility.

Mar. 15 Introduction to Expressivity
Mar. 22 Expressivity
Based on:
C. Palamidessi, "Comparing the Expressive Power of the Synchronous and the Asynchronous π-calculus" (available online)
D. Gorla, "Towards a Unified Approach to Encodability and Separation Results for Process Calculi" (available online)
M. Carbone, S.Maffeis, "On the Expressive Power of Polyadic Synchronisation in π-calculus" (available online)

Mar. 27 Psi calculi
Note: this meeting is on TUESDAY, 14-16 in 4A05
Speaker: Jesper Bengtson
Based on:
J. Bengtson, M. Johansson, J. Parrow, B. Victor, "Psi Calculi: A Framework for Mobile Processes with Nominal Data and Logic" (available here)

Mar. 29 (Easter Break)

Apr. 5 Applied Pi Calculus
Speaker: Alessandro Bruni
Based on:
M. Abadi, C. Fournet, "Mobile Values, New Names and Secure Communication" (available online)
V. Cortier, S. Kremer, "Formal Models and Techniques for Analyzing Security Protocols: A Tutorial" (available online)

Apr. 12 CSP
Speaker: Rosario Giustolisi
Based on:
A.W. Roscoe, "The Theory and Practice of Concurrency" (available online)
S. Schneider, "Concurrent and Real time Systems: The CSP Approach" (available online)

Apr. 19 Weak Bisimilarity in Psi Calculi
Speaker: Jesper Bengtson
Based on:
M. Johansson, J. Bengtson, J. Parrow, B. Victor, "Weak Equivalences in Psi-calculi" (available online)

Apr 26. Binary Session Types
Based on:
K. Honda, V.T. Vasconcelos, M. Kubo, "Language Primitives and Type Discipline for Structured Communication-Based Programming" (available here)

May 3. Multiparty Session Types
Based on:
K. Honda, N. Yoshida, M. Carbone, "Multiparty Asynchronous Session Types" (available online, journal version)

May 10. (Ascention Day)

May 17. Asynchronous Session Types
Speaker: Jonas Kastberg Hinrichsen
Based on:
K. Honda, N. Yoshida, M. Carbone, "Multiparty Asynchronous Session Types" (available online, journal version)

May 24. Linear Logic and Session Types
Speaker: Carsten Schürmann
Based on:
L. Caires, F. Pfening, B. Toninho, "Linear Logic Propositions as Session Types" (available online)

May 31. (Research Sharing Day)

June 7. Classical Processes
Room: 4A05
Based on:
P. Wadler, "Propositions as Sessions" (available online)

June 14. (Cancelled, PLS lunch talk)

June 21. Corecursion and Non-Divergence in Session Types
Room: 4A05
Speaker: Sonia Marin
Based on:
B. Toninho, L. Caires, F. Pfenning "Corecursion and Non-Divergence in Session Types" (available online)

June 26. Guest talk: Logical Foundations for Concurrency: Logical Relations, Non-Determinism, Open Problems
Note: this meeting is on TUESDAY, 10-12, Auditorium 4
Speaker: Jorge A. Perez, University of Groningen

Abstract:

The study of logical foundations for message-passing concurrency has attracted considerable attention. Indeed, the line of work started by Caires, Pfenning, Wadler, and several others, has been extended in multiple directions, including, for instance, dependent types, multiparty protocols, and run-time monitoring. In this presentation, I will discuss two developments: the first is a theory of logical relations for session-typed processes; the second is an extension of the interpretation based on classical linear logic with a form of non-deterministic behaviour. If time allows, I will discuss an open research problem in concurrency theory: how can we make sense of the "jungle" of typed process models?

July 4. Declarative interpretations of session-based concurrency
Note: this meeting is on WEDNESDAY, 10-12, 4A05
Speaker: Alexander Asp Bock
Based on:
M. Cano, C. Rueda, H. A. López, J. A. Pérez "Declarative interpretations of session-based concurrency" (available online)



Course description

The course will focus on concurrency theory and its applications. The first part of the course will consist of 8-10 lectures given by experts in the field, and providing an in-depth introduction to the topic. The program for this part will include the following topics:
  1. Calculus of Communicating Systems
  2. Different kinds of semantics
  3. Synchronous (and asynchronous) Pi calculus
  4. Observable behaviours and bisimulation
  5. Session types and multi-party session types
  6. Expressivity
  7. Connection to linear logic
  8. Choreographies

In the second part, the focus will be put on recent results in concurrency theory. With a solid background provided in the first part, a number of influential papers from the last few years will be discussed in depth. The precise selection will be based on the research interests of the participants.



Reading list (for the first part of the course) includes:

Books
  • R. Milner; Communicating and Mobile Systems: the pi-Calculus
  • R. Milner; Communication and Concurrency
  • D. Sangiorgi, D. Walker; The pi-calculus: a Theory of Mobile Processes
  • S. Gay, A. Ravara; Behavioural Types: From Theory to Tools
  • R. Milner; The Space and Motion of Communicating Agents

Articles
  • D. Gorla; Towards a Unified Approach to Encodability and Separation Results for Process Calculi
  • K. Takeuchi, K.Honda, M. Kubo; An interaction-based language and its typing system
  • K. Honda, N. Yoshida, M. Carbone; Multiparty Asynchronous Session Types
  • L. Caires, F. Pfenning; Session Types as Intuitionistic Linear Propositions
  • P. Wadler; Propositions as Sessions

PhD dissertation
  • F. Montesi; Choreographic Programming