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" (availablehere)

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:

Calculus of Communicating Systems

Different kinds of semantics

Synchronous (and asynchronous) Pi calculus

Observable behaviours and bisimulation

Session types and multi-party session types

Expressivity

Connection to linear logic

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

Thursdays, 10-12Room: 3A18Starting 8th FebruaryPhD 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 SystemsSyntax, semantics, limitations

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

Based on: R. Milner, "Communication and Concurrency"Feb. 22 Pi CalculusBased on: J. Parrow, "An introduction to the pi-calculus" (available online)Mar. 1 True concurrencySpeakers: 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" (availablehere)Mar. 8 Guest talk: Reversible Event StructuresSpeakers: Eva Graversen and Nobuko Yoshida

Imperial College London http://mrg.doc.ic.ac.uk/

AbstractWe 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 ExpressivityMar. 22 ExpressivityBased 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 calculiNote: this meeting is on TUESDAY, 14-16 in 4A05Speaker: 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 CalculusSpeaker: 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 CSPSpeaker: 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 CalculiSpeaker: Jesper Bengtson

Based on:M. Johansson, J. Bengtson, J. Parrow, B. Victor, "Weak Equivalences in Psi-calculi" (available online)Apr 26. Binary Session TypesBased on:K. Honda, V.T. Vasconcelos, M. Kubo, "Language Primitives and Type Discipline for Structured Communication-Based Programming" (available here)May 3. Multiparty Session TypesBased on:K. Honda, N. Yoshida, M. Carbone, "Multiparty Asynchronous Session Types" (available online, journal version)May 10. (Ascention Day)May 17. Asynchronous Session TypesSpeaker: 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 TypesSpeaker: 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 ProcessesRoom: 4A05Based on:P. Wadler, "Propositions as Sessions" (available online)June 14. (Cancelled, PLS lunch talk)June 21. Corecursion and Non-Divergence in Session TypesRoom: 4A05Speaker: 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 ProblemsNote: this meeting is on TUESDAY, 10-12, Auditorium 4Speaker: Jorge A. Perez

,University of GroningenAbstract: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 concurrencyNote: this meeting is on WEDNESDAY, 10-12, 4A05Speaker: 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 descriptionThe 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:

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

Articles

PhD dissertation