Models of concurrency, categories, and games

Description

Mathematical models of concurrent or distributed systems typically belong to one of two families: interleaving models, which represent a concurrent system by enumerating its exponentially many schedulings, and independence models, which instead represent explicitly information of causality or independence between computational events. They address the need for an abstract representation for the behaviour of concurrent or distributed systems, to be used for various purposes, from the semantic study and the design of concurrent programming languages to the formal verification of distributed systems. This course focuses on independence or causal models of concurrency, which are more precise and mathematically elaborate than their interleaving counterparts. The course will introduce various notions of interleaving (transition systems) and independence (Petri nets, Mazurkiewicz trace languages, event structures) models, along with tools for reasoning on them (bisimulation and open maps) and comparisons between them.

The course will then give an introduction to ongoing research in developing a mathematical theory of distributed (or concurrent) games. Games and strategies are very commonly used in logic and computer science (among many other fields), typically to model interactive or open systems. But games considered in the literature often have a very restricted structure: they are sequential, and the players often have to alternate. In contrast the games presented here, based on event structures, allow a Player (or a team of players) to interact and compete against an Opponent (or a team of opponents) in a highly distributed fashion, with no recourse to interleavings. We will illustrate the model by an application to the semantics of a simple concurrent programming language.

All these developments rely on some notions of category theory which we will introduce along the way.

Teachers

• Pierre Clairambault
• Glynn Winskel

Lectures

• Lecture 1 (Glynn, 13/09/17). General motivations (domains, semantics). CCS, Petri nets. Here are the slides.

  You can find additional material on CCS and Petri nets in the Cambridge lecture notes ``Topics in Concurrency'' here.

• Lecture 2 (Pierre, 20/09/17). Basic categories. Universal properties, categories, cartesian categories, coproducts, equalizers, pullbacks, functors, natural transformations.

  Categories, functors, natural transformations: Chapter 1 of Tom Leinster's book.

  Products, equalizers, pullbacks: Section 5.1 of Tom Leinster's book (p.107-117).

• Lecture 3 (Glynn, 27/09/17). Event structures, stable families, maps between those. Here are the slides.

• Lecture 4 (Pierre, 04/10/17). Subcategories, full and faithful functors, functor categories, presheaves, natural isomorphisms, equivalence of categories, dual category, covariance and contravariance, product category, bifunctors, adjunctions via natural bijection.

  Dual category, product category: section 1.1 of the book.

  Subcategories, full and faithful functors, presheaves, covariance/contravariance: section 1.2 of the book.

  Natural isomorphisms, equivalence of categories: section 1.3 of the book.

  Adjunctions via natural bijections: section 2.1 of the book.

• Lecture 5 (Glynn, 11/10/17). Adjunction between event structures and stable families. Same slides.

• Lecture 6 (Pierre, 25/10/17). Vertical/horizontal composition of natural transformations. Adjunctions via unit and co-unit. Examples of units and co-units. Products as representations, right adjoints preserve products.

  Horizontal composition of natural transformations, interchange law: p.37-38 of the book.

  Adjunctions via unit and co-unit: section 2.2 of the book.

• Lecture 7 (Glynn, 08/11/17). Constructions in stable families and event structures. Products, restrictions, pullbacks. Here are the slides, and the course notes.

• Lecture 8 (Pierre, 15/11/17). Overview of denotational semantics, motivations for denotational semantics of concurrent programming languages. Reminder of the lambda-calculus. Adjunctions via cofree objects. Cartesian closed category. Syntactic cartesian closed category, interpretation of the lambda-calculus in a cartesian closed category. Soundness and completeness of the interpretation.

  Cartesian closed categories are covered very briefly in the book (p.165-168), without the connection to the lambda-calculus.

  The reference for the correspondence between cartesian closed categories and the lambda-calculus is the book "Introduction to higher-order categorical logic" by Lambek and Scott, which is not available online. The content of the lecture can also be found (with slightly different notational conventions) in Streicher's notes on categorical logic (p.61-76).

• Lecture 9 (Glynn, 22/11/17). Concurrent strategies. Interaction of concurrent strategies, composition, copycat strategy. Here are the slides and course notes.

• Lecture 10 (Glynn, 29/11/17). Deterministic strategies. slides and course notes.

• Lecture 11 (Pierre, 13/12/17). Monoidal categories, symmetric monoidal categories, compact closed categories, symmetric monoidal closed categories. The compact closed category of concurrent strategies.

Homework

• Subject 1. CCS, Petri nets, and basic categories. To be returned on the 04/10/2017.
• Subject 2. Maps of event structures, and natural transformations. To be returned on the 25/10/2017.
• Subject 3. Games, Strategies and Cartesian Closed Categories. To be returned on the 13/12/2017.

Summary of contents (subject to change)

• Models of concurrency (Glynn Winskel)
  • General motivations: domains, semantics
  • CCS, transition systems, Petri nets
  • Stable families, event structures, unfoldings
  • Event structure model of CCS
• Category theory (Pierre Clairambault)
  • Categories, functors, natural transformations
  • Adjunctions, limits
  • Symmetric monoidal categories and the affine lambda-calculus
  • Compact closed categories, bicategories (?)
• Concurrent games (Pierre Clairambault and Glynn Winskel)
  • Games, strategies, composition
  • Compact closed structure (and the linear lambda-calculus)
  • Concurrent game semantics of programming languages
  • Extensions: probabilities, ...

Prerequisites

References

Models of concurrency

• Glynn Winskel and Mogens Nielsen. Models for concurrency, a chapter in the Handbook of Logic in Computer Science (1993). Oxford University Press.
• Glynn Winskel, Notes for Topics in Concurrency, a Part II Computer Science course at the University of Cambridge, [lecture notes]

Category theory

• Tom Leinster Basic Category Theory, 2016. [book]

Game Semantics

• Samson Abramsky, Guy McCusker, Game Semantics, 1998. [book chapter]
• Glynn Winskel, Notes for Advanced Topics in Concurrency: Concurrent games, a Part III and MPhil Computer Science course at the University of Cambridge, 2014. [lecture notes]

Evaluation

Main evaluation will be a final exam.

Additional evaluation (leading to bonus on the final grade) will be based on homework.