Titles and Abstracts of Papers
Accepted for Presentation at MFPS 19

Ribbon Proofs
Jules Bean, Queen Mary, University of London

We present `Ribbon Proofs', a graphical proof system for the Logic of Bunched Implications (BI). We give the informal, graphical, notation, we formalise the system algebraically and sketch the proof of its soundness and completeness. We discuss the spatial and geometrical nature of the proof system and its relation to BI's spatial model theory.

Cumulative computing
Yifeng Chen Chen, University of Leicester

In this paper we use the concept of resource cumulation to unify computational models of imperative programming. The space of cumulations (called a cumulator) is simply represented as a five tuple consisting of a well-founded partial order, a monoid and a volume function. The volume function is introduced to simplify reasoning about limit points and other topological properties. A specification command is a set of cumulations. Typical phenomena of concurrency such as reactiveness, safety and liveness, fairness, real time and branching time naturally arise from the model. In order to support a programming theory, we introduce a specification language that incorporates sequentiality, nondeterminism, simple parallelism, negation and general recursions. A new fixpoint technique is used to model general recursions. The language is applied to the case study on CSP, which becomes a special model of cumulative computing with a combination of four resource cumulators of alphabet, termination, trace and refusal. All laws of cumulative computing are also valid for CSP and the generalization from CSP to Timed CSP can be achieved by simply combining the four cumulators with real time. Loops whose bodies may take zero time can then be modeled more satisfactorily.

Pseudo-distributive laws
Eugenia Cheng and Martin Hyland, University of Cambridge
and John Power, Edinburgh University

We address the question of how elegantly to combine a number of different structures, such as finite product structure, monoidal structure, and colimiting structure, on a category. Extending work of Marmolejo and Lack, we develop the definition of a pseudo-distributive law between pseudo-monads, and we show how the definition and the main theorems about it may be used to model several such structures simultaneously. Specifically, we address the relationship between pseudo-distributive laws and the lifting of one pseudo-monad to the 2-category of algebras and to the Kleisli bicategory of another. This, for instance, sheds light on the preservation of some structures but not others along the Yoneda embedding. Our leading examples are given by the use of open maps to model bisimulation and by the logic of bunched implications.

Entropic Geometry from Logic
Bob Coecke, Oxford University

A finitary probability space (=all probability measures on a fixed finite support) can be faithfully represented by a partial order equipped with a measure of content (e.g. Shannon entropy).

This partial order can be obtained via a purely order-theoretic systematic procedure starting from an algebra of properties. This procedure applies to any poset envisioned as an algebra of properties.

The Security Picalculus and Non-interference
Matthew Hennessy, University of Sussex

The security picalculus is a typed version of the asynchronous picalculus in which the types, in addition to constraining the input/output behaviour of processes, have security levels associated with them. This enables us to introduce a range of typing disciplines which allow input or output behaviour, or both, to be bounded above or below by a given security level. We define typed versions of may and must equivalences for the security picalculus, where the tests are parameterised relative to a security level. We provide alternative characterisations of these equivalences in terms of actions in context; these describe the actions a process may perform, assuming the observer is constrained by a given typing environment. Using these alternative characterisations we prove non-interference results with respect to may and must testing. These show that information flow between security levels can be controled using our typing systems.

A construction subsuming the Chu construction
Dominic Hughes, Stanford University

We introduce a construction which produces a star-autonomous category from any given set. It subsumes the Chu construction in the sense that the category produced from K contains the category of Chu spaces over K as a full subcategory.

Contextual equivalence for higher-order pi-calculus revisited
Alan Jeffrey, DePaul University and Julian Rathke, University of Sussex


The higher-order pi-calculus is an extension of the pi-calculus to allow communication of abstractions of processes rather than names alone. It has been studied intensively by Sangiorgi in his thesis where a characterisation of a contextual equivalence for higher-order pi-calculus is provided using labelled transition systems and normal bisimulations. Unfortunately the proof technique used there requires a restriction of the language to only allow finite types. We revisit this calculus and offer an alternative presentation of the labelled transition system and a novel proof technique which allows us to provide a fully abstract characterisation of contextual equivalence using labelled transitions and bisimulations for higher-order pi-calculus with recursive types also.

On the semantics of the bad-variable constructor in Algol-like languages
Guy McCusker, COGS, University of Sussex

The fully abstract games model of Reynolds's Idealized Algol is adapted to provide a characterization of the language without the ``bad variable constructor'' mkvar. The model shows that the addition of mkvar to the language is conservative for observational equivalence but not for the observational preorder.

Generic Transforms on Incomplete Specifications of Asynchronous Interfaces
Radu Negulescu, McGill University

In a previous paper, processes constitute incomplete specifications that guarantee behavior only under assumed constraints; and, executions are abstract. Here we define a corresponding notion of morphism, called process abstractions, as maps that preserve a composition operator on processes, and, implicitly, an order relation. A ternary symmetry is revealed between the process space composition operators: product (parallel composition), meet (alternative composition), join, etc., are isomorphic. We characterize process abstractions to be obtained by a generic construction parameterized by a binary relation on executions and by the composition operators involved. We rework in this general framework several correctness-preserving properties of process maps, and we demonstrate the results on several commonly used maps. The generalization has yielded several new operations of independent interest, shown as applications.

How do domains model topologies?
Pawel Waszkiewicz, Jagiellonian University

A model of a topological space X is a continuous poset P such that X is homeomorphic to the subset of maximal elements of P in its subspace Scott topology.

The main objective of this brief survey is to explicitly match the properties of modelled spaces with the structure of their models.

We thus inspect existing construction of models that appeared in the literature and reexamine considerations concerning the space of maximal elements of continuous domains. We claim that every additional structure to the modelled topology is mirrored by some specific construct in the model and vice versa. Examples are pairs:

By making this duality precise and explicit we reveal how domains model topologies. Our exposition is based on author's doctoral dissertation.

Chu spaces, concept lattices, and domains
Guo-Qiang Zhang, Case Western Reserve University

This paper serves to bring three independent but important areas of computer science to a common meeting point: Each area is given a perspective or reformulation that is conducive to the flow of ideas and to the exploration of cross-disciplinary connections. Among other results, we prove (Theorem 4.3) that the notion of states in Scott's information system corresponds precisely to that of formal concepts in FCA with respect to all finite Chu spaces.