Selected Paper of the 33rd Conference on the Mathematical Foundations of Programming Semantics (MFPS 2017)

2017 Editors: Achim Jung, Alexandra Silva

This special issue contains extended versions of papers presented at MFPS XXXIII, the Thirty-third Conference on the Mathematical Foundations of Programming Semantics. The conference was held in Ljubljana, Slovenia, between June 12th and June 15th 2017. MFPS conferences are devoted to those areas of mathematics, logic, and computer science that are related to models of computation, in general, and to the semantics of programming languages, in particular. A core concern of the series is to provide a forum where researchers in mathematics and computer science can meet and exchange ideas about problems of common interest. As the series also strives to maintain breadth in its scope, the conference strongly encourages participation by researchers in neighbouring areas.

This special issue contains revised and extended versions of a small selection of the papers presented at the conference, which\\'a0are a testament to the high quality and the wide range of research presented at MFPS. The submitted extended papers were reviewed in accordance with the usual high standards of LMCS, receiving two or three additional reviews.

We thank the program committee of MFPS XXXIII for their help in the selection process, and the experts who agreed to review the papers submitted to this special issue, providing timely and constructive suggestions to improve the papers. And we also thank all the authors for their care and work in improving their submissions.

Alexandra Silva, Achim Jung
Guest Editors of the MFPS XXXIII Special Issue

1. A categorical foundation for structured reversible flowchart languages: Soundness and adequacy

Robert Glück ; Robin Kaarsgaard.

Structured reversible flowchart languages is a class of imperative reversible programming languages allowing for a simple diagrammatic representation of control flow built from a limited set of control flow structures. This class includes the reversible programming language Janus (without recursion), as well as more recently developed reversible programming languages such as R-CORE and R-WHILE. In the present paper, we develop a categorical foundation for this class of languages based on inverse categories with joins. We generalize the notion of extensivity of restriction categories to one that may be accommodated by inverse categories, and use the resulting decisions to give a reversible representation of predicates and assertions. This leads to a categorical semantics for structured reversible flowcharts, which we show to be computationally sound and adequate, as well as equationally fully abstract with respect to the operational semantics under certain conditions.

2. Stone-Type Dualities for Separation Logics

Simon Docherty ; David Pym.

Stone-type duality theorems, which relate algebraic and relational/topological models, are important tools in logic because -- in addition to elegant abstraction -- they strengthen soundness and completeness to a categorical equivalence, yielding a framework through which both algebraic and topological methods can be brought to bear on a logic. We give a systematic treatment of Stone-type duality for the structures that interpret bunched logics, starting with the weakest systems, recovering the familiar BI and Boolean BI (BBI), and extending to both classical and intuitionistic Separation Logic. We demonstrate the uniformity and modularity of this analysis by additionally capturing the bunched logics obtained by extending BI and BBI with modalities and multiplicative connectives corresponding to disjunction, negation and falsum. This includes the logic of separating modalities (LSM), De Morgan BI (DMBI), Classical BI (CBI), and the sub-classical family of logics extending Bi-intuitionistic (B)BI (Bi(B)BI). We additionally obtain as corollaries soundness and completeness theorems for the specific Kripke-style models of these logics as presented in the literature: for DMBI, the sub-classical logics extending BiBI and a new bunched logic, Concurrent Kleene BI (connecting our work to Concurrent Separation Logic), this is the first time soundness and completeness theorems have been proved. We thus obtain a comprehensive semantic account of the multiplicative variants of all […]

3. Proving Soundness of Extensional Normal-Form Bisimilarities

Dariusz Biernacki ; Serguei Lenglet ; Piotr Polesiuk.

Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in $\lambda$-calculi by decomposing their normal forms into bisimilar subterms. Moreover, it typically allows for powerful up-to techniques, such as bisimulation up to context, which simplify bisimulation proofs even further. However, proving soundness of these relations becomes complicated in the presence of $\eta$-expansion and usually relies on ad hoc proof methods which depend on the language. In this paper we propose a more systematic proof method to show that an extensional normal-form bisimilarity along with its corresponding up to context technique are sound. We illustrate our technique with three calculi: the call-by-value $\lambda$-calculus, the call-by-value $\lambda$-calculus with the delimited-control operators shift and reset, and the call-by-value $\lambda$-calculus with the abortive control operators call/cc and abort. In the first two cases, there was previously no sound up to context technique validating the $\eta$-law, whereas no theory of normal-form bisimulations for a calculus with call/cc and abort has been presented before. Our results have been fully formalized in the Coq proof assistant.

4. A Denotational Semantics for SPARC TSO

Ryan Kavanagh ; Stephen Brookes.

The SPARC TSO weak memory model is defined axiomatically, with a non-compositional formulation that makes modular reasoning about programs difficult. Our denotational approach uses pomsets to provide a compositional semantics capturing exactly the behaviours permitted by SPARC TSO. It uses buffered states and an inductive definition of execution to assign an input-output meaning to pomsets. We show that our denotational account is sound and complete relative to the axiomatic account, that is, that it captures exactly the behaviours permitted by the axiomatic account. Our compositional approach facilitates the study of SPARC TSO and supports modular analysis of program behaviour.

5. Distances between States and between Predicates

Bart Jacobs ; Abraham Westerbaan.

This paper gives a systematic account of various metrics on probability distributions (states) and on predicates. These metrics are described in a uniform manner using the validity relation between states and predicates. The standard adjunction between convex sets (of states) and effect modules (of predicates) is restricted to convex complete metric spaces and directed complete effect modules. This adjunction is used in two state-and-effect triangles, for classical (discrete) probability and for quantum probability.

6. Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory

Mathys Rennela ; Sam Staton.

We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a crucial role. Following earlier work on QWire by Paykin et al., we consider both a simple first-order linear language for circuits, and a more powerful host language, such that the circuit language is embedded inside the host language. Our categorical semantics for the host language is standard, and involves cartesian closed categories and monads. We interpret the circuit language not in an ordinary category, but in a category that is enriched in the host category. We show that this structure is also related to linear/non-linear models. As an extended example, we recall an earlier result that the category of W*-algebras is dcpo-enriched, and we use this model to extend the circuit language with some recursive types.