2017

We introduce a new class of (dynamical) systems that inherently capture cascading effects (viewed as consequential effects) and are naturally amenable to combinations. We develop an axiomatic general theory around those systems, and guide the endeavor towards an understanding of cascading failure. […]

We extend the constructive dependent type theory of the Logical Framework $\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates over judgements, called Locks. These monads capture various possible proof attitudes in establishing the judgment of the object logic encoded by […]

The class of uniformly computable real functions with respect to a small subrecursive class of operators computes the elementary functions of calculus, restricted to compact subsets of their domains. The class of conditionally computable real functions with respect to the same class of operators is […]

In this paper we investigate important categories lying strictly between the Kleisli category and the Eilenberg-Moore category, for a Kock-Z\"oberlein monad on an order-enriched category. Firstly, we give a characterisation of free algebras in the spirit of domain theory. Secondly, we study the […]

The Internet of Things (IoT) offers the infrastructure of the information society. It hosts smart objects that automatically collect and exchange data of various kinds, directly gathered from sensors or generated by aggregations. Suitable coordination primitives and analysis mechanisms are in order […]

We propose new sequent calculus systems for orthologic (also known as minimal quantum logic) which satisfy the cut elimination property. The first one is a simple system relying on the involutive status of negation. The second one incorporates the notion of focusing (coming from linear logic) to […]

Quasi-trees generalize trees in that the unique "path" between two nodes may be infinite and have any countable order type. They are used to define the rank-width of a countable graph in such a way that it is equal to the least upper-bound of the rank-widths of its finite induced […]

Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of the left-hand sides; the computational intuition is that rules cannot build new data structures. In programming language research, cons-free languages have been used […]

The algebraic intersection type unification problem is an important component in proof search related to several natural decision problems in intersection type systems. It is unknown and remains open whether the algebraic intersection type unification problem is decidable. We give the first […]

In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One way to prove this would be to remark that Markov's principle does not hold in a sheaf model of type theory over Cantor space, since Markov's principle does not hold for […]

Information flow is the branch of security that studies the leakage of information due to correlation between secrets and observables. Since in general such correlation cannot be avoided completely, it is important to quantify the leakage. The most followed approaches to defining […]

For a quantale ${\sf{V}}$, the category $\sf V$-${\bf Top}$ of ${\sf{V}}$-valued topological spaces may be introduced as a full subcategory of those ${\sf{V}}$-valued closure spaces whose closure operation preserves finite joins. In generalization of Barr's characterization of topological spaces […]

In this paper, we define a new realizability semantics for the simply typed lambda-mu-calculus. We show that if a term is typable, then it inhabits the interpretation of its type. We also prove a completeness result of our realizability semantics using a particular term model. This paper corrects […]

We prove that connectors are stable under quotients in any (regular) Goursat category. As a consequence, the category $\mathsf{Conn}(\mathbb{C})$ of connectors in $\mathbb{C}$ is a Goursat category whenever $\mathbb C$ is. This implies that Goursat categories can be characterised in terms of a […]

Section:
Algebraic methods

Session contracts is a formalism enabling to investigate client/server interaction protocols and to interpret session types. We extend session contracts in order to represent outputs whose actual sending in an interaction depends on a third party or on a mutual agreement between the partners. […]

We show that the first order theory of the lattice of open sets in some natural topological spaces is $m$-equivalent to second order arithmetic. We also show that for many natural computable metric spaces and computable domains the first order theory of the lattice of effectively open sets is […]

Normalisation in probability theory turns a subdistribution into a proper distribution. It is a partial operation, since it is undefined for the zero subdistribution. This partiality makes it hard to reason equationally about normalisation. A novel description of normalisation is given as […]

In the context of protomodular categories, several additional conditions have been considered in order to obtain a closer group-like behavior. Among them are locally algebraic cartesian closedness and algebraic coherence. The recent notion of S-protomodular category, whose main examples are the […]

Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are quantitative extensions of linear temporal logic, which are prominent and widely used in the verification of real-timed systems. It was recently shown that the path checking problem for MTL, when evaluated over finite […]

Notions of simulation, among other uses, provide a computationally tractable and sound (but not necessarily complete) proof method for language inclusion. They have been comprehensively studied by Lynch and Vaandrager for nondeterministic and timed systems; for Büchi automata the notion of […]

This paper investigates second-order representations in the sense of Kawamura and Cook for spaces of integrable functions that regularly show up in analysis. It builds upon prior work about the space of continuous functions on the unit interval: Kawamura and Cook introduced a representation inducing […]

We extend the notion of localic completion of generalised metric spaces by Steven Vickers to the setting of generalised uniform spaces. A generalised uniform space (gus) is a set X equipped with a family of generalised metrics on X, where a generalised metric on X is a map from the product of X to […]

The edit distance between two words $w_1, w_2$ is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform $w_1$ to $w_2$. The edit distance generalizes to languages $\mathcal{L}_1, \mathcal{L}_2$, where the edit distance from $\mathcal{L}_1$ […]

The well-quasi-ordering (i.e., a well-founded quasi-ordering such that all antichains are finite) that defines well-structured transition systems (WSTS) is shown not to be the weakest hypothesis that implies decidability of the coverability problem. We show coverability decidable for monotone […]

We give a new order-theoretic characterization of a complete Heyting and co-Heyting algebra $C$. This result provides an unexpected relationship with the field of Nash equilibria, being based on the so-called Veinott ordering relation on subcomplete sublattices of $C$, which is crucially used in […]

The computation of the winning set for parity objectives and for Streett objectives in graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness conditions, the verification of open […]

We present sound and complete environmental bisimilarities for a variant of Dybvig et al.'s calculus of multi-prompted delimited-control operators with dynamic prompt generation. The reasoning principles that we obtain generalize and advance the existing techniques for establishing program […]

Traditionally, formal languages are defined as sets of words. More recently, the alternative coalgebraic or coinductive representation as infinite tries, i.e., prefix trees branching over the alphabet, has been used to obtain compact and elegant proofs of classic results in language theory. In this […]

The winning condition of a parity game with costs requires an arbitrary, but fixed bound on the cost incurred between occurrences of odd colors and the next occurrence of a larger even one. Such games quantitatively extend parity games while retaining most of their attractive properties, i.e, […]

We consider a special case of Dickson's lemma: for any two functions $f,g$ on the natural numbers there are two numbers $i<j$ such that both $f$ and $g$ weakly increase on them, i.e., $f_i\le f_j$ and $g_i \le g_j$. By a combinatorial argument (due to the first author) a simple bound for such […]

Presentations of categories are a well-known algebraic tool to provide descriptions of categories by means of generators, for objects and morphisms, and relations on morphisms. We generalize here this notion, in order to consider situations where the objects are considered modulo an […]

We show that, for a quantale $V$ and a $\mathsf{Set}$-monad $\mathbb{T}$ laxly extended to $V$-$\mathsf{Rel}$, the presheaf monad on the category of $(\mathbb{T},V)$-categories is simple, giving rise to a lax orthogonal factorisation system (lofs) whose corresponding weak factorisation system […]

Kleene algebra axioms are complete with respect to both language models and binary relation models. In particular, two regular expressions recognise the same language if and only if they are universally equivalent in the model of binary relations. We consider Kleene allegories, i.e., Kleene algebras […]

In this paper we give an arithmetical proof of the strong normalization of lambda-Sym-Prop of Berardi and Barbanera [1], which can be considered as a formulae-as-types translation of classical propositional logic in natural deduction style. Then we give a translation between […]

In 2011, Rideau and Winskel introduced concurrent games and strategies as event structures, generalizing prior work on causal formulations of games. In this paper we give a detailed, self-contained and slightly-updated account of the results of Rideau and Winskel: a notion of pre-strategy based on […]