Volume 13, Issue 3

2017


1. Towards an Algebra for Cascade Effects

Adam, Elie M. ; Dahleh, Munther A. ; Ozdaglar, Asuman.
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. […]

2. $\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads

Honsell, Furio ; Liquori, Luigi ; Maksimovic, Petar ; Scagnetto, Ivan.
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 […]

3. Characterization theorem for the conditionally computable real functions

Georgiev, Ivan.
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 […]

4. Aspects of algebraic Algebras

Hofmann, Dirk ; Sousa, Lurdes.
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 […]

5. Tracing where IoT data are collected and aggregated

Bodei, Chiara ; Degano, Pierpaolo ; Ferrari, Gian-Luigi ; Galletta, Letterio.
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 […]

6. Focusing in Orthologic

Laurent, Olivier.
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 […]

7. Algebraic and logical descriptions of generalized trees

Courcelle, Bruno.
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 […]

8. Complexity Hierarchies and Higher-order Cons-free Term Rewriting

Kop, Cynthia ; Simonsen, Jakob Grue.
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 […]

9. The Algebraic Intersection Type Unification Problem

Dudenhefner, Andrej ; Martens, Moritz ; Rehof, Jakob.
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 […]

10. The Independence of Markov's Principle in Type Theory

Coquand, Thierry ; Mannaa, Bassel.
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 […]

11. On the Compositionality of Quantitative Information Flow

Kawamoto, Yusuke ; Chatzikokolakis, Konstantinos ; Palamidessi, Catuscia.
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 […]

12. A Note on the Topologicity of Quantale-Valued Topological Spaces

Lai, Hongliang ; Tholen, Walter.
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 […]