ABSTRACT. We study chemical reaction networks (CRNs) as a kernel language for concurrency models with semantics based on ordinary differential equations. We study the problem of comparing two CRNs, i.e., to decide whether the trajectories of a source CRN can be matched by a target CRN under an appropriate choice of initial conditions. Using a categorical framework, we extend and relate model-comparison approaches based on structural (syntactic) and on dynamical (semantic) properties of a CRN, proving their equivalence. Then, we provide an algorithm to compare CRNs, running linearly in time with respect to the cardinality of all possible comparisons. Finally, we apply our results to biological models from the literature.

ABSTRACT. In his 1986 Automatica paper Willems developed the influential behavioural approach to control theory with an investigation of linear discrete-time time-invariant (LTI) dynamical systems. The behavioural approach places open systems at its centre, modelling by ‘tearing, zooming, and linking’. In this paper, we show that these ideas are naturally expressed in the language of symmetric monoidal categories. Our main result then implies an intuitive sound and complete string diagram algebra for reasoning about LTI systems. These string diagrams are closely related to the classical notion of signal flow graphs, but in contrast to previous work, they are endowed with a semantics that is standard in control theory: they are understood as multi-input multi-output transducers that process streams with an infinite past as well as an infinite future. At the categorical level, the algebraic characterisation is that of the prop of linear corelations instead of the prop of linear relations. We derive a novel structural characterisation of controllability, and consequently provide a methodology for analysing controllability of networked and interconnected systems. We argue that this methodology has the potential of providing elegant, simple and efficient solutions to problems arising in the analysis of systems over networks, a vibrant research area at the crossing of control theory and computer science.

ABSTRACT. Hybrid systems (also called cyber-physical systems, or CPSs), such as computer- controlled cars, airplanes or robots play an increasingly crucial role in our daily lives. They are systems that we bet our lives on, so they need to be safe. However, ensuring that such hybrid systems are safe is an intellectual challenge due to their intricate interactions of discrete control software with physical behavior. Formal verification techniques, such as theorem proving, can provide strong guarantees for these systems by returning proofs that safety is preserved throughout the continuously infinite space of their possible behaviors.

We introduce differential refinement logic (dRL), a logic with first-class support for refinement relations on hybrid systems, and a proof calculus for verifying such relations. The logic dRL simultaneously solves several seemingly different challenges common in theorem proving for hybrid systems: 1. When hybrid systems are complicated, it is useful to prove properties about simpler and related subsystems before tackling the system as a whole. 2. Some models of hybrid systems can be implementation-specific. Verification can be aided by abstracting the system down to the core components necessary for safety, but only if the relations between the abstraction and the original system can be guaranteed. 3. One approach to taming the complexities of hybrid systems is to start with a simplified version of the system and iteratively expand it. However, this approach can be costly, since every iteration has to be proved safe from scratch, unless refinement relations can be leveraged in the proof. 4. When proofs become large, it is difficult to maintain a modular or comprehensible proof structure. By using a refinement relation to arrange proofs hierarchically according to the structure of natural subsystems, we can increase the readability and modularity of the resulting proof.

The logic dRL extends an existing specification and verification language for hybrid systems (differential dynamic logic, dL) by adding a refinement relation to directly compare hybrid systems. This paper gives a syntax, semantics, and proof calculus for dRL. We also demonstrate the usefulness of dRL on several examples. We show that using refinement results in easier and better-structured proofs, leveraging as first- class citizens in the proof the structure that has only been implicit in previous dL proofs.

ABSTRACT. The continuous evolution of a wide variety of systems, including continous- time Markov chains and linear hybrid automata, is described in terms of linear differential equations. In this paper we study the decision problem of whether the solution x(t) of a system of linear differential equations dx/dt=Ax reaches a target halfspace infinitely often. This recurrent reachability problem can equivalently be formulated as the following Infinite Zeros Problem: does a real-valued function f:R->R satisfying a given linear differential equation have infinitely many zeros over the non-negative reals? Our main decidability result is that if the differential equation has order at most 7, then the Infinite Zeros Problem is decidable. On the other hand, we show that a decision procedure for the Infinite Zeros Problem at order 9 (and above) would entail a major breakthrough in Diophantine Approximation, specifically an algorithm for computing the Lagrange constants of arbitrary real algebraic numbers to arbitrary precision.

ABSTRACT. We study the semantic foundation of expressive probabilistic programming languages, that support higher-order functions, continuous distributions, and soft constraints (such as Anglican, Church, and Venture). We define a metalanguage (an idealised version of Anglican) for probabilistic computation with the above features, develop both operational and denotational semantics, and prove soundness, adequacy, and termination. They involve measure theory, stochastic labelled transition systems, and functor categories, but admit intuitive computational readings, one of which views sampled random variables as dynamically allocated read-only variables. We apply our semantics to validate nontrivial equations underlying the correctness of certain compiler optimisations and inference algorithms such as sequential Monte Carlo simulation. The language enables defining probability distributions on higher-order functions, and we study their properties.

ABSTRACT. Theories featuring the interaction between a Frobenius algebra and a Hopf algebra have recently appeared in several areas in computer science: concurrent programming, control theory, and quantum computing, among others. Bonchi, Sobocinski, and Zanasi have shown that, given a suitable distribution law, a pair of Hopf algebras forms two frobenius algebras. Coming from the perspective of quantum theory, we take the opposite approach, and show that interacting Frobenius algebras form Hopf algebras. We generalise \cite{Bonchi2014a} by including non-trivial dynamics of the underlying object---the so-called phase group---and investigate the effects of finite dimensionality of the underlying model, and recover the system of Bonchi et al as a subtheory in the prime power dimensional case. We show that the presence of a non-trivial phase group means that the theory cannot be formalised as a distributive law.

ABSTRACT. Recently, Eilenberg's variety theorem was reformulated in the light of Stone's duality theorem. On one level, this reformulation led to a unification of several existing Eilenberg-type theorems and further generalization of these theorems. On another level, this reformulation is also a natural continuation of the research line on profinite monoids that has been developed since the late 1980's in this field. The current paper concerns the latter in particular. In this relation, this paper introduces and studies the class of semi-galois categories, i.e. an extension of galois categories; and provides particularly fundamental results concerning semi-galois categories and the classical Eilenberg variety theory: that is, (I) a duality theorem between profinite monoids and semi-galois categories; (II) a coherent duality-based reformulation of two classical Eilenberg-type variety theorems due to Straubing and Chaubard, Pin, and Straubing; and (III) a Galois-type classification of closed subgroups of profinite monoids in terms of finite discrete cofibrations over semi-galois categories.

ABSTRACT. Combining insights from the study of type refinement systems and of monoidal closed chiralities, we show how to reconstruct Lawvere's hyperdoctrine of presheaves using a full and faithful embedding into a monoidal closed bifibration living now over the compact closed category of small categories and distributors. Besides revealing dualities which are not immediately apparent in the traditional presentation of the presheaf hyperdoctrine, this reconstruction leads us to an axiomatic treatment of directed equality predicates (modelled by $\hom$ presheaves), realizing a vision initially set out by Lawvere (1970). It also leads to a simple calculus of string diagrams (representing presheaves) that is highly reminiscent of C.~S.~Peirce's existential graphs for predicate logic, refining an earlier interpretation of existential graphs in terms of Boolean hyperdoctrines by Brady and Trimble. Finally, we illustrate how this work extends to a bifibrational setting a number of fundamental ideas of linear logic.

ABSTRACT. This paper contributes to recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory. We present a mechanized proof of a result called the Blakers-Massey connectivity theorem, which relates the higher-dimensional loop structures of two spaces sharing a common part (represented by a _pushout type_, which is a generalization of a disjoint sum type) to those of the common part itself. This theorem gives important information about the pushout type, and has a number of useful corollaries. The proof is more direct than existing ones that apply in general category-theoretic settings for homotopy theory, and its mechanization is concise and high-level, due to novel combinations of ideas from homotopy theory and from type theory.

ABSTRACT. In intuitionistic realizability like Kleene's or Kreisel's, the full axiom of choice is trivially realized. It is even provable in Martin-Löf's intuitionistic type theory. In classical logic, however, even the weaker axiom of countable choice proves the existence of non-computable functions. This logical strength comes at the price of a complicated computational interpretation which involves strong recursion schemes like bar recursion. We take the best from both worlds and define a realizability model for arithmetic and the axiom of choice which encompasses both intuitionistic and classical reasoning. In this model two versions of the axiom of choice can co-exist in a single proof: intuitionistic choice and classical countable choice. We interpret intuitionistic choice efficiently, however its premise cannot come from classical reasoning. Conversely, our version of classical choice is valid in full classical logic, but it is restricted to the countable case and its realizer involves bar recursion. Having both versions allows us to obtain efficient extracted programs while keeping the provability strength of classical logic.

ABSTRACT. We introduce a trace semantics for a call-by-value language with full polymorphism and higher-order references. This is an operational game semantics model based on a nominal interpretation of parametricity whereby polymorphic values are abstracted with special kinds of names. The use of polymorphic references leads to violations of parametricity which we counter by closely recoding the disclosure of typing information in the semantics. We prove the model sound for the full language and strengthen our result to full abstraction for a large fragment where polymorphic references obey specific inhabitation conditions.

ABSTRACT. Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to define equalities (paths). We say that a HIT H is non-recursive if its constructors do not quantify over elements or paths in H. The advantage of non-recursive HITs is that their elimination principles are easier to apply than those of general HITs. It is an open question which classes of HITs can be encoded as non-recursive HITs. One result of this paper is the construction of the propositional truncation via a sequence of approximations, yielding a representation as a non-recursive HIT. Compared to a related construction by van Doorn, ours has the advantage that the connectedness level increases in each step, yielding simplified elimination principles into n-types. As the elimination principle of our sequence has strictly lower requirements, we can then prove a similar result for van Doorn's construction. We further de rive general elimination principles of higher truncations (say, k-truncations) into n-types, generalizing a previous result by Capriotti et al. which considered the case n ≡ k + 1. The results have been formalized in Agda.

ABSTRACT. We introduce 2-compactness, a constructive function-theoretic alternative to topological compactness, based on the notions of Bishop space and Bishop morphism, constructive function-theoretic alternatives to topological space and continuous function, respectively. We show that the Bishop morphism is reduced to uniform continuity in important cases, it generalizes metric compactness, as the uniformly continuous functions on a compact metric space form a 2-compact Bishop topology, and we prove a countable Tychonoff compactness theorem for 2-compact spaces. We work within BISH*, Bishop's informal system of constructive mathematics BISH equipped with inductive definitions with rules of countably many premisses.

ABSTRACT. We prove that an $\omega$-categorical core structure primitively positively interprets all finite structures with parameters if and only if some stabilizer of its polymorphism clone has a homomorphism to the clone of projections, and that this happens if and only if its polymorphism clone does not contain operations $\alpha$, $\beta$, $s$ satisfying the identity $\alpha s(x,y,x,z,y,z) \approx \beta s(y,x,z,x,z,y)$.

This establishes an algebraic criterion equivalent to the conjectured borderline between P and NP-complete CSPs over reducts of finitely bounded homogenous structures, and accomplishes one of the steps of a proposed strategy for reducing the infinite domain CSP dichotomy conjecture to the finite case.

Our theorem is also of independent mathematical interest, characterizing a topological property of any $\omega$-categorical core structure (the existence of a continuous homomorphism of a stabilizer of its polymorphism clone to the projections) in purely algebraic terms (the failure of an identity as above).

ABSTRACT. Many natural decision problems can be formulated as constraint satisfaction problems for reducts of finitely bounded homogeneous structures. This class of problems is a large generalisation of the class of CSPs over finite domains. Our first result is a general polynomial-time reduction from such infinite-domain CSPs to finite-domain CSPs. We use this reduction to obtain powerful new polynomial-time tractability conditions that can be expressed in terms of topological polymorphism clones. Moreover, we study the subclass C of CSPs for structures that are first-order definable over equality with parameters. Also this class C properly extends the class of all finite-domain CSPs. We formulate a tractability conjecture for C and show that it is equivalent to the finite-domain tractability conjecture. In our proof we develop new algebraic techniques that help to prove continuity of certain clone homomorphisms needed for showing hardness.

ABSTRACT. The characterization of all the Constraint Satisfaction Problems of bounded width, proposed by Feder and Vardi [SICOMP'98], was confirmed in [Bulatov'09] and independently in [FOCS'09, JACM'14]. Both proofs are based on the (2,3)-consistency (using Prague consistency in [FOCS'09], directly in [Bulatov'09]) which is costly to verify.

We introduce a new consistency notion, Singleton Linear Arc Consistency (SLAC), and show that it solves the same family of problems. SLAC is weaker than Singleton Arc Consistency (SAC) and thus the result answers the question from [JLC'13] by showing that SAC solves all the problems of bounded width. At the same time the problem of verifying weaker consistency (even SAC) offers significant computational advantages over the problem of verifying (2,3)-consistency which improves the algorithms solving the CSPs of bounded width.

ABSTRACT. In our LICS 2004 paper we introduced an approach to the study of the local structure of finite algebras that aims at applications in the Constraint Satisfaction Problem (CSP). This approach involves a graph associated with an algebra A or a relational structure, whose vertices are the elements of A, the edges represent subsets of A such that the restriction of some term operation of A is `good' on the subset, that is, act as an operation of one of the 3 types: semilattice, majority, or affine. In this paper we significantly refine and advance this approach. In particular, we prove rectangularity properties of relations over algebras related to components of the graph connected by semilattice and affine edges. We also prove a result similar to 2-decomposition of relations invariant under a majority operation, only here we do not impose any restrictions on the relation. These results allow us to give a new, somewhat more intuitive proof of the bounded width theorem: the CSP over algebra A has bounded width if and only if A does not contain affine edges. We also consider algebras with edges from a restricted set of types. In particular, it can be proved that type restrictions are preserved under the standard algebraic constructions. Finally, we prove that algebras without semilattice edges have few subalgebras of powers, that is, the CSP over such algebras is also solvable in polynomial time.

ABSTRACT. Characterising tractable fragments of the constraint satisfaction problem (CSP) is an important challenge in theoretical computer science and artificial intelligence. Forbidding patterns (generic sub-instances) provides a means of defining CSP fragments which are neither exclusively language-based nor exclusively structure-based. It is known that the class of binary CSP instances in which the broken-triangle pattern (BTP) does not occur, a class which includes all tree-structured instances, are decided by arc consistency (AC), a ubiquitous reduction operation in constraint solvers. We provide a characterisation of irreducible partially-ordered forbidden patterns which have this AC-solvability property. It turns out that BTP is just one of five such AC-solvable patterns. The four other patterns allow us to exhibit new tractable classes.