# Volume 13, Issue 1

2017

### 1. Logical compactness and constraint satisfaction problems

We investigate a correspondence between the complexity hierarchy of constraint satisfaction problems and a hierarchy of logical compactness hypotheses for finite relational structures. It seems that the harder a constraint satisfaction problem is, the stronger the corresponding […]

### 2. Mixed powerdomains for probability and nondeterminism

We consider mixed powerdomains combining ordinary nondeterminism and probabilistic nondeterminism. We characterise them as free algebras for suitable (in)equation-al theories; we establish functional representation theorems; and we show equivalencies between state transformers and appropriately […]

### 3. Stream Differential Equations: Specification Formats and Solution Methods

Streams, or infinite sequences, are infinite objects of a very simple type, yet they have a rich theory partly due to their ubiquity in mathematics and computer science. Stream differential equations are a coinductive method for specifying streams and stream operations, and their theory has been […]

### 4. Unprovability of circuit upper bounds in Cook's theory PV

We establish unconditionally that for every integer $k \geq 1$ there is a language $L \in \mbox{P}$ such that it is consistent with Cook's theory PV that $L \notin Size(n^k)$. Our argument is non-constructive and does not provide an explicit description of this language.

### 5. A feasible interpolation for random resolution

Random resolution, defined by Buss, Kolodziejczyk and Thapen (JSL, 2014), is a sound propositional proof system that extends the resolution proof system by the possibility to augment any set of initial clauses by a set of randomly chosen clauses (modulo a technical condition). We show how to apply […]

### 6. Complexity of Conditional Term Rewriting

We propose a notion of complexity for oriented conditional term rewrite systems satisfying certain restrictions. This notion is realistic in the sense that it measures not only successful computations, but also partial computations that result in a failed rule application. A transformation […]

### 7. Sequential decision problems, dependent types and generic solutions

We present a computer-checked generic implementation for solving finite-horizon sequential decision problems. This is a wide class of problems, including inter-temporal optimizations, knapsack, optimal bracketing, scheduling, etc. The implementation can handle time-step dependent control and state […]

### 8. Lineal: A linear-algebraic Lambda-calculus

We provide a computational definition of the notions of vector space and bilinear functions. We use this result to introduce a minimal language combining higher-order computation and linear algebra. This language extends the Lambda-calculus with the possibility to make arbitrary linear […]

### 9. Reasoning about Strategies: on the Satisfiability Problem

Strategy Logic (SL, for short) has been introduced by Mogavero, Murano, and Vardi as a useful formalism for reasoning explicitly about strategies, as first-order objects, in multi-agent concurrent games. This logic turns out to be very powerful, subsuming all major previously studied modal logics […]

### 10. A Coordination Language for Databases

We present a coordination language for the modeling of distributed database applications. The language, baptized Klaim-DB, borrows the concepts of localities and nets of the coordination language Klaim but re-incarnates the tuple spaces of Klaim as databases. It provides high-level abstractions […]

### 11. Termination of Cycle Rewriting by Transformation and Matrix Interpretation

We present techniques to prove termination of cycle rewriting, that is, string rewriting on cycles, which are strings in which the start and end are connected. Our main technique is to transform cycle rewriting into string rewriting and then apply state of the art techniques to prove termination […]

### 12. Reachability Analysis of Innermost Rewriting

We consider the problem of inferring a grammar describing the output of a functional program given a grammar describing its input. Solutions to this problem are helpful for detecting bugs or proving safety properties of functional programs, and several rewriting tools exist for solving this problem. […]

### 13. Asynchronous Distributed Execution Of Fixpoint-Based Computational Fields

Coordination is essential for dynamic distributed systems whose components exhibit interactive and autonomous behaviors. Spatially distributed, locally interacting, propagating computational fields are particularly appealing for allowing components to join and leave with little or no overhead. […]

### 14. Typing weak MSOL properties

We consider lambda-Y-calculus as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as the tree of calls to built-in operations. Weak monadic second-order logic (wMSOL) is well suited to express properties of such trees. We […]

### 15. Notions of Anonymous Existence in Martin-L\"of Type Theory

As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in […]

### 16. Minimisation of Multiplicity Tree Automata

We consider the problem of minimising the number of states in a multiplicity tree automaton over the field of rational numbers. We give a minimisation algorithm that runs in polynomial time assuming unit-cost arithmetic. We also show that a polynomial bound in the standard Turing model would require […]

### 17. Multiparty Session Actors

Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type (MPST) protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions […]

### 18. Existence of strongly proper dyadic subbases

We consider a topological space with its subbase which induces a coding for each point. Every second-countable Hausdorff space has a subbase that is the union of countably many pairs of disjoint open subsets. A dyadic subbase is such a subbase with a fixed enumeration. If a dyadic subbase is given, […]