In this paper we introduce Event Identifier Logic (EIL), which extends Hennessy–Milner logic by the addition of:

1. (1) reverse as well as forward modalities; and

2. (2) identifiers to keep track of events.

We introduce Horn linear logic as a comprehensive logical system capable of handling the typical AI problem of making a plan of the actions to be performed by a robot so that he could get into a set of final situations, if he started with a certain initial situation. Contrary to undecidability of propositional Horn linear logic, the planning problem is proved to be decidable for a reasonably wide class of natural robot systems.

The planning problem is proved to be EXPTIME-complete for the robot systems that allow actions with non-deterministic effects. Fixing a finite signature, that is a finite set of predicates and their finite domains, we get a polynomial time procedure of making plans for the robot system over this signature.

The planning complexity is reduced to PSPACE for the robot systems with only pure deterministic actions.

As honest numerical parameters in our algorithms we invoke the length of description of a planning task ‘from W to Z˜’ and the Kolmogorov descriptive complexity of AxT, a set of possible actions.

Light affine logic is a variant of linear logic with a polynomial cut-elimination procedure. We study the extensional expressive power of light affine logic with respect to a general notion of encoding of functions in the setting of the Curry–Howard correspondence. We consider light affine logic with both fixpoints of formulae and second-order quantifiers, and analyse the properties of polytime soundness and polytime completeness for various fragments of this system. In particular, we show that the implicative propositional fragment is not polytime complete if we place some reasonable conditions on the encodings. Following previous work, we show that second order leads to polytime unsoundness. We then introduce simple constraints on second-order quantification and fixpoints, and prove that the fragments obtained are polytime sound and complete.

We present a realisability model for a call-by-value, higher-order programming language with parametric polymorphism, general first-class references, and recursive types. The main novelty is a relational interpretation of open types that include general reference types. The interpretation uses a new approach to modelling references.

The universe of semantic types consists of world-indexed families of logical relations over a universal predomain. In order to model general reference types, worlds are finite maps from locations to semantic types: this introduces a circularity between semantic types and worlds that precludes a direct definition of either. Our solution is to solve a recursive equation in an appropriate category of metric spaces. In effect, types are interpreted using a Kripke logical relation over a recursively defined set of worlds.

We illustrate how the model can be used to prove simple equivalences between different implementations of imperative abstract data types.

Two imperative programming language phrases interfere when one writes to a storage variable that the other reads from or writes to. Reynolds has described an elegant linguistic approach to controlling interference in which a refinement of typed λ-calculus is used to limit sharing of storage variables; in particular, different identifiers are required never to interfere. This paper examines semantic foundations of the approach.

We describe a category that has (an abstraction of) interference information built into all objects and maps. This information is used to define a ‘tensor’ product whose components are required never to interfere. Environments are defined using the tensor, and procedure types are obtained via a suitable adjunction. The category is a model of intuitionistic linear logic. Reynolds' concept of passive type - i.e. types for phrases that do not write to any storage variables - is shown to be closely related, in this model, to Girard's ‘of course’ modality.

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-preserving (H-H) bisimulation. Since H-H bisimulation may be characterised by the use of reverse as well as forward transitions, it is of interest to investigate these and other forms of bisimulations where both forward and reverse transitions are allowed. Bednarczyk asked whether SB with reverse steps is as strong as H-H bisimulation. We answer this question negatively. We give various characterisations of SB with reverse steps, showing that forward steps do not add power. We strengthen Bednarczyk's result that, in the absence of auto-concurrency, reverse IB is as strong as H-H bisimulation, by showing that we need only exclude auto-concurrent events at the same depth in the configuration.

We consider several other forms of observations of reversible behaviour and define a wide range of bisimulations by mixing the forward and reverse observations. We investigate the power of these bisimulations and represent the relationships between them as a hierarchy with IB at the bottom and H-H at the top.

Linear bicategories are a generalization of bicategories in which the one horizontal composition is replaced by two (linked) horizontal compositions. These compositions provide a semantic model for the tensor and par of linear logic: in particular, as composition is fundamentally non-commutative, they provide a suggestive source of models for non-commutative linear logic.

In a linear bicategory, the logical notion of complementation becomes a natural linear notion of adjunction. Just as ordinary adjoints are related to (Kan) extensions, these linear adjoints are related to the appropriate notion of linear extension.

There is also a stronger notion of complementation, which arises, for example, in cyclic linear logic. This sort of complementation is modelled by cyclic adjoints. This leads to the notion of a *ast;-linear bicategory and the coherence conditions that it must satisfy. Cyclic adjoints also give rise to linear monads: these are, essentially, the appropriate generalization (to the linear setting) of Frobenius algebras and the ambialgebras of Topological Quantum Field Theory.

A number of examples of linear bicategories arising from different sources are described, and a number of constructions that result in linear bicategories are indicated.

This paper shows how it is possible to express many techniques of categorical domain theory in the general context of topical categories (where ‘topical’ means internal in the category Top of Grothendieck toposes with geometric morphisms). The underlying topos machinery is hidden by using a geometric form of constructive mathematics, which enables toposes as ‘generalized topological spaces’ to be treated in a transparently spatial way, and also shows the constructivity of the arguments. The theory of strongly algebraic (SFP) domains is given as a case study in which the topical category is Cartesian closed.

String diagrams are a powerful tool for reasoning about physical processes, logic circuits, tensor networks and many other compositional structures. The distinguishing feature of these diagrams is that edges need not be connected to vertices at both ends, and these unconnected ends can be interpreted as the inputs and outputs of a diagram. In this paper, we give a concrete construction for string diagrams using a special kind of typed graph called an open-graph. While the category of open-graphs is not itself adhesive, we introduce the notion of a selective adhesive functor, and show that such a functor embeds the category of open-graphs into the ambient adhesive category of typed graphs. Using this functor, the category of open-graphs inherits ‘enough adhesivity’ from the category of typed graphs to perform double-pushout (DPO) graph rewriting. A salient feature of our theory is that it ensures rewrite systems are ‘type safe’ in the sense that rewriting respects the inputs and outputs. This formalism lets us safely encode the interesting structure of a computational model, such as evaluation dynamics, with succinct, explicit rewrite rules, while the graphical representation absorbs many of the tedious details. Although topological formalisms exist for string diagrams, our construction is discrete and finitary, and enjoys decidable algorithms for composition and rewriting. We also show how open-graphs can be parameterised by graphical signatures, which are similar to the monoidal signatures of Joyal and Street, and define types for vertices in the diagrammatic language and constraints on how they can be connected. Using typed open-graphs, we can construct free symmetric monoidal categories, PROPs and more general monoidal theories. Thus, open-graphs give us a tool for mechanised reasoning in monoidal categories.

Session types and contracts are two formalisms used to study client–server protocols. In this paper, we study the relationship between them. The main result is the existence of a fully abstract model of session types; this model is based on a natural interpretation of these types into a subset of contracts.

Activities such as clinical investigations (CIs) or financial processes are subject to regulations to ensure quality of results and avoid negative consequences. Regulations may be imposed by multiple governmental agencies as well as by institutional policies and protocols. Due to the complexity of both regulations and activities, there is great potential for violation due to human error, misunderstanding, or even intent. Executable formal models of regulations, protocols and activities can form the foundation for automated assistants to aid planning, monitoring and compliance checking. We propose a model based on multiset rewriting where time is discrete and is specified by timestamps attached to facts. Actions, as well as initial, goal and critical states may be constrained by means of relative time constraints. Moreover, actions may have non-deterministic effects, i.e. they may have different outcomes whenever applied. We present a formal semantics of our model based on focused proofs of linear logic with definitions. We also determine the computational complexity of various planning problems. Plan compliance problem, for example, is the problem of finding a plan that leads from an initial state to a desired goal state without reaching any undesired critical state. We consider all actions to be balanced, i.e. their pre- and post-conditions have the same number of facts. Under this assumption on actions, we show that the plan compliance problem is PSPACE-complete when all actions have only deterministic effects and is EXPTIME-complete when actions may have non-deterministic effects. Finally, we show that the restrictions on the form of actions and time constraints taken in the specification of our model are necessary for decidability of the planning problems.

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 formalism is general enough to include models like weighted modal transition systems and allows system developers to employ more complex label refinement than in previously studied theories. On the other hand, the formalism maintains the desirable properties required by any specification theory supporting compositional reasoning. In particular, we study modal and thorough refinement, determinisation, parallel composition, conjunction, quotient and logical characterisation of label-structured modal transition systems.

Categorical constructions inherent to a theory of algebras with strict partial operations are presented and exploited to provide a categorical deduction calculus for conditional existence equations and an alternative definition of such algebras based on the notion of syntactic categories. A compact presentation of the structural theory of parameterized (partial) specifications is given using the categorical approach. This theory is shown to be suitable for providing initial semantics as well as the compositionality results necessary for the definition of specification languages like ACT ONE and ACT TWO

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 it is resource conscious and gives the programmer suitable primitives to handle explicitly the resources used by a program during its execution. The differential operator also allows us to write the full Taylor expansion of a program. Through this expansion, every program can be decomposed into an infinite sum (representing non-deterministic choice) of ‘simpler’ programs that are strictly linear.

The aim of this paper is to develop an abstract ‘model theory’ for the untyped differential λ-calculus. In particular, we investigate what form a general categorical definition of a denotational model for this calculus should take. Starting from the work of Blute, Cockett and Seely on differential categories, we develop the notion of a Cartesian closed differential category and prove that linear reflexive objects living in such categories constitute sound and complete models of the untyped differential λ-calculus. We also give sufficient conditions for Cartesian closed differential categories to model the Taylor expansion. This requires that every model living in such categories equates all programs having the same full Taylor expansion.

We then provide a concrete example of a Cartesian closed differential category modelling the Taylor expansion, namely the category MRel of sets and relations from finite multisets to sets. We prove that the extensional model of λ-calculus we have recently built in MRel is linear, and is thus also an extensional model of the untyped differential λ-calculus. In the same category, we build a non-extensional model and prove that it is, nevertheless, extensional on its differential part.

Finally, we study the relationship between the differential λ-calculus and the resource calculus, which is a functional programming language combining the ideas behind the differential λ-calculus with those behind Boudol's λ-calculus with multiplicities. We define two translation maps between these two calculi and study the properties of these translations. In particular, this analysis shows that the two calculi share the same notion of a model, and thus that the resource calculus can be interpreted by translation into every linear reflexive object living in a Cartesian closed differential category.

In recent times, satisfiability modulo theories (SMT) techniques gained increasing attention and obtained remarkable success in model-checking infinite-state systems. Still, we believe that whenever more expressivity is needed in order to specify the systems to be verified, more and more support is needed from mathematical logic and model theory. This is the case of the applications considered in this paper: we study verification over a general model of relational, data-aware processes, to assess (parameterized) safety properties irrespectively of the initial database (DB) instance. Toward this goal, we take inspiration from array-based systems and tackle safety algorithmically via backward reachability. To enable the adoption of this technique in our rich setting, we make use of the model-theoretic machinery of model completion, which surprisingly turns out to be an effective tool for verification of relational systems and represents the main original contribution of this paper. In this way, we pursue a twofold purpose. On the one hand, we isolate three notable classes for which backward reachability terminates, in turn witnessing decidability. Two of such classes relate our approach to conditions singled out in the literature, whereas the third one is genuinely novel. On the other hand, we are able to exploit SMT technology in implementations, building on the well-known MCMT (Model Checker Modulo Theories) model checker for array-based systems and extending it to make all our foundational results fully operational. All in all, the present contribution is deeply rooted in the long-standing tradition of the application of model theory in computer science. In particular, this paper applies these ideas in an original mathematical context and shows how these techniques can be used for the first time to empower algorithmic techniques for the verification of infinite-state systems based on arrays, so as to make such techniques applicable to the timely, challenging settings of data-aware processes.

The study of type theory may offer a uniform language for modular programming, structured specification and logical reasoning. We develop an approach to program specification and data refinement in a type theory with a strong logical power and nice structural mechanisms to show that it provides an adequate formalism for modular development of programs and specifications. Specification of abstract data types is considered, and a notion of abstract implementation between specifications is defined in the type theory and studied as a basis for correct and modular development of programs by stepwise refinement. The higher-order structural mechanisms in the type theory provide useful and flexible tools (specification operations and parameterized specifications) for modular design and structured specification. Refinement maps (programs and design decisions) and proofs of implementation correctness can be developed by means of the existing proof development systems based on type theories.

This is the second instalment in the project initiated in Manin (2012). In the first Part, we argued that both the philosophy and technique of perturbative renormalisation in quantum field theory could be meaningfully transplanted to the theory of computation, and sketched several contexts supporting this view.

In this second part, we address some of the issues raised in Manin (2012) and develop them further in three contexts: a categorification of the algorithmic computations; time cut-off and anytime algorithms; and, finally, a Hopf algebra renormalisation of the Halting Problem.

Over recent decades there has been a trend towards formalised mathematics, and a number of sophisticated systems have been developed both to support the formalisation process and to verify the results mechanically. However, each tool is based on a specific foundation of mathematics, and formalisations in different systems are not necessarily compatible. Therefore, the integration of these foundations has received growing interest. We contribute to this goal by using LF as a foundational framework in which the mathematical foundations themselves can be formalised and therefore also the relations between them. We represent three of the most important foundations – Isabelle/HOL, Mizar and ZFC set theory – as well as relations between them. The relations are formalised in such a way that the framework permits the extraction of translation functions, which are guaranteed to be well defined and sound. Our work provides the starting point for a systematic study of formalised foundations in order to compare, relate and integrate them.

The density matrices of graphs are combinatorial laplacians normalised to have trace one (Braunstein et al. 2006b). If the vertices of a graph are arranged as an array, its density matrix carries a block structure with respect to which properties such as separability can be considered. We prove that the so-called degree-criterion, which was conjectured to be necessary and sufficient for the separability of density matrices of graphs, is equivalent to the PPT-criterion. As such, it is not sufficient for testing the separability of density matrices of graphs (we provide an explicit example). Nonetheless, we prove the sufficiency when one of the array dimensions has length two (see Wu (2006) for an alternative proof). Finally, we derive a rational upper bound on the concurrence of density matrices of graphs and show that this bound is exact for graphs on four vertices.

This special issue of Mathematical Structures in Computer Science contains several contributions related to the modern field of Quantum Information and Quantum Computing.

The first two papers deal with entanglement. The paper by R. Mosseri and P. Ribeiro presents a detailed description of the two- and three-qubit geometry in Hilbert space, dealing with the geometry of fibrations and discrete geometry. The paper by J.-G.Luque et al. is more algebraic and considers invariants of pure k-qubit states and their application to entanglement measurement.