Published: 27th August 2020 DOI: 10.4204/EPTCS.322 ISSN: 2075-2180 |
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 |
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
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.
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.
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.