Published: 27th August 2020
DOI: 10.4204/EPTCS.322
ISSN: 2075-2180

EPTCS 322

Proceedings Combined 27th International Workshop on
Expressiveness in Concurrency
and 17th Workshop on
Structural Operational Semantics
Online, 31 August 2020

Edited by: Ornela Dardha and Jurriaan Rot

Preface
Ornela Dardha and Jurriaan Rot
Invited Presentation: Quantitative Algebraic Reasoning: an Overview
Giorgio Bacci
1
Invited Presentation: Divergence-Preserving Branching Bisimilarity
Bas Luttik
3
Invited Presentation: Multiparty Session Programming with Global Protocol Combinators
Rumyana Neykova
12
Can determinism and compositionality coexist in RML?
Davide Ancona, Angelo Ferrando and Viviana Mascardi
13
A process algebra with global variables
Mark Bouwman, Bas Luttik, Wouter Schols and Tim A.C. Willemse
33
Reactive Temporal Logic
Rob van Glabbeek
51
Substructural Observed Communication Semantics
Ryan Kavanagh
69
Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell's MVars
Manfred Schmidt-Schauß and David Sabel
88

Preface

This volume contains the proceedings of EXPRESS/SOS 2020, the Combined 27th International Workshop on Expressiveness in Concurrency and the 17th Workshop on Structural Operational Semantics. Following a long tradition, EXPRESS/SOS 2020 was held as one of the affiliated workshops of the 31st International Conference on Concurrency Theory (CONCUR 2020), originally planned to be held in Vienna, Austria. Due to the covid-19 pandemic, it was instead held online as a virtual workshop.

The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models. In particular, topics of interest for the workshop include (but are not limited to):

This year, the Program Committee selected 6 submissions for inclusion in the scientific program - five full papers and the following short paper:

This volume contains revised versions of the given full papers, as well as (extended) abstracts associated to the following three invited presentations, which nicely complemented the scientific program:

We would like to thank the authors of the submitted papers, the invited speakers, the members of the program committee, and their subreviewers for their contribution to both the meeting and this volume. We also thank the CONCUR 2020 organizing committee for hosting the workshop. Finally, we would like to thank our EPTCS editor Rob van Glabbeek for publishing these proceedings and his help during the preparation.

Ornela Dardha and Jurriaan Rot,
August 2020

Program Committee

Additional Reviewers

Johannes Åman Pohjola
Frank Valencia

Quantitative Algebraic Reasoning: an Overview

Giorgio Bacci (Aalborg University)

Some Context and Motivations

Moggi's approach [6, 7] of incorporating computational effects in higher-order functional programming languages via the use of monads posed the basis for a unified category theoretic semantics for computational effects such as nondeterminism, probabilistic nondeterminism, side-effects, exceptions, etc. His semantics makes a careful systematic distinction between computational effects and values. A computation may be pure, in which case it terminates and returns a value, or effectful, in which case it performs a side-effect encapsulated into a monad structure. The first programming language integrating this idea was Haskell, offering pre-built definitions in its core library; but with the influence of functional programming into other paradigms, formulations of monads (in spirit if not in name) can be found also in popular languages such as Python, Scala, and F#.

Moggi's work was followed up by the program of Plotkin and Power [9, 8, 10] on understanding computational effects as arising from operations and equations (see also the survey of Hyland and Power [3]). The original insight by Plotkin and Power was that many computational effects are naturally described by algebraic theories, and that computations should be described as operations on an algebra. The most profound result in [9] is a generalisation of the correspondence between finitary monads and Lawvere theories from Set to a category with finite products C and a strong monad T on C. This result characterises generic algebraic effects, that is, computational effects described by operations and equations and interpreted on categories possibly richer than Set. A key motivating example from [8] shows how one is allowed to consider computational effects resulting from the solutions of recursive operations by interpreting them in the category of ω-cpo's.

With the emergence of probabilistic programming, which is characterised by the use of probabilistic nondeterminism as build-in computational effect, more emphasis has been put on quantitative reasoning. One thinks in terms of ``how close are two programs?'' rather than ``are they completely indistinguishable?''. This concept is captured by a metric and was first advocated in [2]. To address this need, Mardare et al. [4] proposed a version of equational reasoning, which they call quantitative equational logic, that captures such metric reasoning principles and, crucially, characterises algebraic effects on the category of metric spaces.

Abstract

In this talk I will review the basic definitions, constructions and key results presented in three works, [4, 5, 1], which constitute the first steps of the more ambitious the program of understanding the algebraic properties of computational effects on categories enriched over (extended) metric spaces. During the talk I will provide several motivating examples to offer a general pragmatic picture of how algebraic reasoning works and how it can be used. Finally, I will conclude by presenting a list of open problems and initial ideas on how to address them.

References

  1. Giorgio Bacci, Radu Mardare, Prakash Panangaden & Gordon D. Plotkin (2018): An Algebraic Theory of Markov Processes. In: LICS, ACM, pp. 679–688, doi:10.1145/3209108.3209177.
  2. Alessandro Giacalone, Chi-Chang Jou & Scott A. Smolka (1990): Algebraic Reasoning for Probabilistic Concurrent Systems. In: Programming Concepts and Methods, IFIP TC2, North-Holland, pp. 443–458.
  3. Martin Hyland & John Power (2007): The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads. Electron. Notes Theor. Comput. Sci. 172, pp. 437–458, doi:10.1016/j.entcs.2007.02.019.
  4. Radu Mardare, Prakash Panangaden & Gordon D. Plotkin (2016): Quantitative Algebraic Reasoning. In: LICS, ACM, pp. 700–709, doi:10.1145/2933575.2934518.
  5. Radu Mardare, Prakash Panangaden & Gordon D. Plotkin (2017): On the axiomatizability of quantitative algebras. In: LICS, IEEE Computer Society, pp. 1–12, doi:10.1109/LICS.2017.8005102.
  6. Eugenio Moggi (1988): The Partial Lambda Calculus. Ph.D. thesis, University of Edinburgh. College of Science and Engineering. School of Informatics.
  7. Eugenio Moggi (1991): Notions of Computation and Monads. Inf. Comput. 93(1), pp. 55–92, doi:10.1016/0890-5401(91)90052-4.
  8. Gordon D. Plotkin & John Power (2001): Adequacy for Algebraic Effects. In: FoSSaCS, Lecture Notes in Computer Science 2030, Springer, pp. 1–24, doi:10.1007/3-540-45315-6_1.
  9. Gordon D. Plotkin & John Power (2001): Semantics for Algebraic Operations. In: MFPS, Electronic Notes in Theoretical Computer Science 45, Elsevier, pp. 332–345, doi:10.1016/S1571-0661(04)80970-8.
  10. Gordon D. Plotkin & John Power (2002): Notions of Computation Determine Monads. In: FoSSaCS, Lecture Notes in Computer Science 2303, Springer, pp. 342–356, doi:10.1007/3-540-45931-6_24.

Multiparty Session Programming with Global Protocol Combinators

Rumyana Neykova (Brunel University London)

Multiparty Session Types (MPST) is a typing discipline for communication protocols. It ensures the absence of communication errors and deadlocks for well-typed communicating processes. The state-of-the-art implementations of the MPST theory rely on (1) runtime linearity checks to ensure correct usage of communication channels and (2) external domain-specific languages for specifying and verifying multiparty protocols.

In this talk I will present a library for programming with global combinators - a set of functions for writing and verifying multiparty protocols in OCaml, that overcomes the above limitations. Local behaviours for all processes in a protocol are inferred at once from a global combinator. We formalise global combinators and prove a sound realisability of global combinators - a well-typed global combinator derives a set of local types, by which typed endpoint programs can ensure type and communication safety. Our approach enables fully-static verification and implementation of the whole protocol, from the protocol specification to the process implementations, to happen in the same language.

I will show the implementation in OCaml and will discuss its expressive power and performance. Our work has several distinctive features. It is the first fully-static MPST implementation; it realises multiparty communication over binary channels; it is lightweight - verification of protocols is reduced to type checking; and expressive - we have implemented a plethora of protocols (e.g OAuth, DNS, SMTP). This talk is based on a joint work with Keigo Imai, Nobuko Yoshida, and Shoji Yuen.