The order-enriched category of monotonic predicate transformers over posets is a model of the refinement calculus of higher order imperative programs and pre-post specifications. This category is shown to be equivalent to the category of spans over ideal relations, and ideal relations are shown to be spans over monotonic functions between posets. To do this we use a skew span construction because the standard categorical span constructions are inapplicable. Axioms are given for products and coproducts of underlying posets as well as the homset as a coexponent, using inequations (for various kinds of lax adjunctions) and conditional equations (for adjunctions in subcategories) that are shown to uniquely determine the structures. The model is described in elementary terms using power allegories, an axiomatic calculus of relations, which makes the proofs accessible to non-specialists and shows that the results generalize to other base categories.

This paper introduces a temporal logic for coalgebras. Nexttime and lasttime operators are defined for a coalgebra, acting on predicates on the state space. They give rise to what is called a Galois algebra. Galois algebras form models of temporal logics like Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). The mapping from coalgebras to Galois algebras turns out to be functorial, yielding indexed categorical structures. This construction gives many examples, for coalgebras of polynomial functors on sets. More generally, it will be shown how ‘fuzzy’ predicates on metric spaces, and predicates on presheaves, yield indexed Galois algebras, in basically the same coalgebraic manner.

The spatial search problem consists of minimising the number of steps required to find a given site in a network, with the restriction that only an oracle query or a translation to a neighbouring site is allowed at each step. We propose a quantum algorithm for the spatial search problem on a triangular lattice with N sites and torus-like boundary conditions. The proposed algorithm is a special case of the general framework for abstract search proposed by Ambainis, Kempe and Rivosh (AKR) in Ambainis et al. (2005) and Tulsi in Tulsi (2008) applied to a triangular network. The AKR–Tulsi formalism was employed to show that the time complexity of the quantum search on the triangular lattice is .

We show how the principal typing property of the rank 2 intersection type system enables the specification of a modular and polyvariant control-flow analysis.

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.

We study autostability spectra relative to strong constructivizations (SC-autostability spectra). For a decidable structure $\mathcal{S}$, the SC-autostability spectrum of $\mathcal{S}$ is the set of all Turing degrees capable of computing isomorphisms among arbitrary decidable copies of $\mathcal{S}$. The degree of SC-autostability for $\mathcal{S}$ is the least degree in the spectrum (if such a degree exists).

We prove that for a computable successor ordinal α, every Turing degree c.e. in and above 0(α) is the degree of SC-autostability for some decidable structure. We show that for an infinite computable ordinal β, every Turing degree c.e. in and above 0(2β+1) is the degree of SC-autostability for some discrete linear order. We prove that the set of all PA-degrees is an SC-autostability spectrum. We also obtain similar results for autostability spectra relative to n-constructivizations.

In the first part of this paper (Duval and Reynaud 1994), we defined a categorical framework, based on the notion of sketch, for specification and evaluation in the senses of algebraic specifications and algebraic programming. Static evaluation in quasi-projective sketches was defined in Part I; in this paper, dynamic evaluation is introduced. It deals with more general structures, which may have no initial model. Until now, this process has not been used in algebraic specification systems, but computer algebra systems are beginning to use it as a basic tool. Finally, we give some applications of dynamic evaluation to computation in field extensions.

We consider a calculus for multiparty sessions enriched with security levels for messages. We propose a monitored semantics for this calculus, which blocks the execution of processes as soon as they attempt to leak information. We illustrate the use of this semantics with various examples, and show that the induced safety property is compositional and that it is strictly included between a typability property and a security property proposed for an extended calculus in previous work.

We provide a consistent way of looking at a range of finite state machines and their algebraic models. Our claim is that the natural representation of transitions of finite state machines is in terms of monoid homomorphisms, and distinct generalisation processes that can be applied to finite state machines correspond to distinct categorical generalisation processes at the level of the algebraic models.

The generalisations we consider are those from deterministic to non-deterministic machines, from one-way to two-way machines, and from read-only machines to read/write machines. Hence the finite state machines we consider, and provide algebraic models for, are (deterministic and non-deterministic) finite state automata, two-way automata, Mealy machines, and bounded Turing machines.

The categorical constructions corresponding to these generalisation processes are, respectively: altering the base category from functions to relations, applying the Geometry of Interaction, or Int construction, and a categorical process, which we refer to as the Comp construction, that uses the tensor on monoidal categories to construct graded categories.

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.

The effective use of model-based formal methods in the development of complex embedded systems requires the integration of discrete-event models of controllers with continuous-time models of their environments. This paper proposes a new approach to the development of such combined models (co-models), in which an initial discrete-event model may include approximations of continuous-time behaviour that can subsequently be replaced by couplings to continuous-time models. An operational semantics of co-simulation allows the discrete and continuous models to run on their respective simulators and managed by a coordinating co-simulation engine. This permits the exploration of the composite co-model's behaviour in a range of operational scenarios. The approach has been realised using the Vienna Development Method (VDM) as the discrete-event formalism, and 20-sim as the continuous-time framework, and has been applied successfully to a case study based on the distributed controller for a personal transporter device.

The strict globular ω-categories formalize the execution paths of a parallel automaton and the homotopies between them. One associates to such (and any) ω-category [Cscr ] three homology theories. The first one is called the globular homology. It contains the oriented loops of [Cscr ]. The two other ones are called the negative (respectively, positive) corner homology. They contain in a certain manner the branching areas of execution paths or negative corners (respectively, the merging areas of execution paths or positive corners) of [Cscr ]. Two natural linear maps called the negative (respectively, the positive) Hurewicz morphism from the globular homology to the negative (respectively, positive) corner homology are constructed. We explain the reason why these constructions allow the reinterpretation of some geometric problems coming from computer science.

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.

We introduce convex–concave duality for various models of non-deterministic choice, probabilistic choice and the two of them combined. This complements the well-known duality of stably compact spaces in a pleasing way: convex–concave duality swaps angelic and demonic choice, and leaves probabilistic choice invariant.

We show that real-number computations in the interval-domain environment are ‘inherently parallel’ in a precise mathematical sense. We do this by reducing computations of the weak parallel-or operation on the Sierpinski domain to computations of the addition operation on the interval domain.

In this paper we consider general probabilistic theories pertaining to circuits that satisfy two very natural assumptions. We provide a formalism that is local in the following very specific sense: calculations pertaining to any region of space–time employ only mathematical objects associated with that region. We call this formalism locality. It incorporates the idea that space and time should be treated on an equal footing. Formulations that use a foliation of space--time to evolve a state do not have this property, nor do histories-based approaches. An operation has inputs and outputs (through which systems travel), for example,

We examine the problem of finding fully abstract translations between programming languages, i.e., translations that preserve code equivalence and nonequivalence. We present three examples of fully abstract translations: one from call-by-value to lazy PCF, one from call-by-name to call-by-value PCF, and one from lazy to call-by-value PCF. The translations yield lower bounds on decision procedures for proving equivalences of code. We define a notion of ‘functional translation’ that captures the essence of the proofs of full abstraction, and show that some languages cannot be translated into others.

We use some results of Trnková to show first that subcoalgebras are always closed under finite intersections. Assuming that the type functor F is bounded, we obtain a concrete representation of the terminal F-coalgebra. We also provide several equivalent characterizations of boundedness.

Event-driven programming is one of the major paradigms in concurrent and communication-based programming, where events are typically detected as the arrival of messages on asynchronous channels. Unfortunately, the flexibility and performance of traditional event-driven programming come at the cost of more complex programs: low-level APIs and the obfuscation of event-driven control flow make programs difficult to read, write and verify.

This paper introduces a π-calculus with session types that models event-driven session programming (called ESP) and studies its behavioural theory. The main characteristics of the ESP model are asynchronous, order-preserving message passing, non-blocking detection of event/message arrivals and dynamic inspection of session types. Session types offer formal safety guarantees, such as communication and event handling safety, and programmatic benefits that overcome problems with existing event-driven programming languages and techniques. The new typed bisimulation theory developed for the ESP model is distinct from standard synchronous or asynchronous bisimulation, capturing the semantic nature of eventful session-based processes. The bisimilarity coincides with reduction-closed barbed congruence.

We demonstrate the features and benefits of ESP and the behavioural theory through two key use cases. First, we examine an encoding and the semantic behaviour of the event selector, a central component of general event-driven systems, providing core results for verifying type-safe event-driven applications. Second, we examine the Lauer–Needham duality, building on the selector encoding and bisimulation theory to prove that a systematic transformation from multithreaded to event-driven session processes is type- and semantics-preserving.

Using physical experiments as oracles for algorithms, we can characterise the computational power of classes of physical systems. Here we show that two different physical models of the apparatus for a single experiment can have different computational power. The experiment is the scatter machine experiment (SME), which was first presented in Beggs and Tucker (2007b). Our first physical model contained a wedge with a sharp vertex that made the experiment non-deterministic with constant runtime. We showed that Turing machines with polynomial time and an oracle based on a sharp wedge computed the non-uniform complexity class P/poly. Here we reconsider the experiment with a refined physical model where the sharp vertex of the wedge is replaced by any suitable smooth curve with vertex at the same point. These smooth models of the experimental apparatus are deterministic. We show that no matter what shape is chosen for the apparatus:

1. (i) the time of detection of the scattered particles increases at least exponentially with the size of the query; and

2. (ii) Turing machines with polynomial time and an oracle based on a smooth wedge compute the non-uniform complexity class P/log* ⫋ P/poly.