In this paper we extend the spectral order of Coecke and Martin to infinite-dimensional quantum states. Many properties present in the finite-dimensional case are preserved, but some of the most important are lost. The order is constructed and its ...

This paper introduces and studies a categorical analogue of the familiar monoid semiring construction. By introducing an axiomatisation of summation that unifies notions of summation from algebraic program semantics with various notions of summation ...

Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow the hiding of irrelevant parts of the state during verification, whereas the anti-frame rule allows the hiding of local state from the ...

We propose an alternative approach, based on diagram rewriting, for computations in bialgebras. We illustrate this graphical syntax by proving some properties of co-operations, including coassociativity and cocommutativity. This amounts to checking the ...

We introduce homotopical methods based on rewriting on higher-dimensional categories to prove coherence results in categories with an algebraic structure. We express the coherence problem for (symmetric) monoidal categories as an asphericity problem for ...

This paper reports on an investigation into the role of shuffling and concatenation in the theory of graph drawing. A simple syntactic description of these and related operations is proved to be complete in the context of finite partial orders, and as ...

The problem of the commutativity of algebraic (categorical) diagrams has attracted the attention of researchers for a long time. For example, the related notion of coherence was discussed in Mac Lane's homology book Mac Lane (1963), see also his AMS ...

In this short note we study the semantics of two basic computational effects, exceptions and states, from a new point of view. In the handling of exceptions we dissociate the control from the elementary operation that recovers from the exception. In ...

We study bialgebras and Hopf algebras in the compact closed category Rel of sets and binary relations. Various monoidal categories with extra structure arise as the categories of (co)modules of bialgebras and Hopf algebras in Rel. In particular, for any ...

We introduce a novel formalism of label-structured modal transition systems that combines the classical may/must modalities on transitions with structured labels that represent quantitative aspects of the model. On the one hand, the specification ...

Quasi-interpretations are a technique for guaranteeing complexity bounds on first-order functional programs: in particular, with termination orderings, they give a sufficient condition for a program to be executable in polynomial time (Marion and Moyen ...

Using the concept of a generalised priority constraint satisfaction problem, we previously found a way to introduce priority queries into fuzzy relational databases. The results were PFSQL (Priority Fuzzy Structured Query Language) together with a ...

The differential λ-calculus is a paradigmatic functional programming language endowed with a syntactical differentiation operator that allows the application of a program to an argument in a linear way. One of the main features of this language is that ...

In this paper we propose a novel approach for analysing proof nets of Multiplicative Linear Logic (MLL) using coding theory. We define families of proof structures called PS-families and introduce a metric space for each family. In each family:

• an MLL ...

Consider the first-order theory of a category.d It has a sort of objects, and a sort of arrows (so we may think of it as a small category). We show that, assuming the principle of unique substitutions, the setoids inside a type theoretic universe ...

In this paper we introduce relative formal topology so that we can deal constructively with the closed subsets of a topological space as well as with the open ones. In fact, within standard formal topology, the cover relation allows the definition of ...

We extend the theory of labelled Markov processes to include internal non-determinism, which is a fundamental concept for the further development of a process theory with abstraction on non-deterministic continuous probabilistic systems. We define non-...

We give a logic-independent semantics for predefined (data) types within the categorical abstract model theoretic framework of the theory of institutions. We develop a generic interpolation result for this semantics, which can be easily applied to ...

Van Glabbeek and Goltz (and later Fecher) have investigated the relationships between various equivalences on stable configuration structures, including interleaving bisimulation (IB), step bisimulation (SB), pomset bisimulation and hereditary history-...

This paper presents a bisimulation-based method for establishing the soundness of equations between terms constructed using operations whose semantics are specified by rules in the GSOS format of Bloom, Istrail and Meyer. The method is inspired by de ...