Volume 13, Issue 2


1. Dynamic Choreographies: Theory And Implementation

Preda, Mila Dalla ; Gabbrielli, Maurizio ; Giallorenzo, Saverio ; Lanese, Ivan ; Mauro, Jacopo.
Programming distributed applications free from communication deadlocks and race conditions is complex. Preserving these properties when applications are updated at runtime is even harder. We present a choreographic approach for programming updatable, distributed applications. We define a […]

2. Subcomputable Schnorr Randomness

Sureson, Claude.
The notion of Schnorr randomness refers to computable reals or computable functions. We propose a version of Schnorr randomness for subcomputable classes and characterize it in different ways: by Martin L\"of tests, martingales or measure computable machines.

3. Hopf and Lie algebras in semi-additive Varieties

Porst, Hans-E..
We study Hopf monoids in entropic semi-additive varieties with an emphasis on adjunctions related to the enveloping monoid functor and the primitive element functor. These investigations are based on the concept of the abelian core of a semi-additive variety variety and its monoidal structure in […]
Section: Coalgebraic methods

4. Certifying Confluence Proofs via Relative Termination and Rule Labeling

Nagele, Julian ; Felgenhauer, Bertram ; Zankl, Harald.
The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on […]

5. Inter-procedural Two-Variable Herbrand Equalities

Frielinghaus, Stefan Schulze ; Petter, Michael ; Seidl, Helmut.
We prove that all valid Herbrand equalities can be inter-procedurally inferred for programs where all assignments whose right-hand sides depend on at most one variable are taken into account. The analysis is based on procedure summaries representing the weakest pre-conditions for finitely many […]

6. A Recipe for State-and-Effect Triangles

Jacobs, Bart.
In the semantics of programming languages one can view programs as state transformers, or as predicate transformers. Recently the author has introduced state-and-effect triangles which capture this situation categorically, involving an adjunction between state- and predicate-transformers. The […]

7. Feasible Interpolation for QBF Resolution Calculi

Beyersdorff, Olaf ; Chew, Leroy ; Mahajan, Meena ; Shukla, Anil.
In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. In this paper we establish the feasible interpolation technique for all resolution-based QBF systems, whether modelling CDCL or expansion-based solving. This both provides the […]

8. A Reduced Semantics for Deciding Trace Equivalence

Baelde, David ; Delaune, Stéphanie ; Hirschi, Lucca.
Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e., without replication) by means of symbolic execution and […]

9. On Sessions and Infinite Data

Severi, Paula ; Padovani, Luca ; Tuosto, Emilio ; Dezani-Ciancaglini, Mariangiola.
We define a novel calculus that combines a call-by-name functional core with session-based communication primitives. We develop a typing discipline that guarantees both normalisation of expressions and progress of processes and that uncovers an unexpected interplay between evaluation and […]

10. Disjoint-union partial algebras

Hirsch, Robin ; McLean, Brett.
Disjoint union is a partial binary operation returning the union of two sets if they are disjoint and undefined otherwise. A disjoint-union partial algebra of sets is a collection of sets closed under disjoint unions, whenever they are defined. We provide a recursive first-order axiomatisation of […]

11. Hanf numbers via accessible images

Lieberman, Michael ; Rosicky, Jiri.
We present several new model-theoretic applications of the fact that, under the assumption that there exists a proper class of almost strongly compact cardinals, the powerful image of any accessible functor is accessible. In particular, we generalize to the context of accessible categories the […]

12. On the Preciseness of Subtyping in Session Types

Chen, Tzu-chun ; Dezani-Ciancaglini, Mariangiola ; Scalas, Alceste ; Yoshida, Nobuko.
Subtyping in concurrency has been extensively studied since early 1990s as one of the most interesting issues in type theory. The correctness of subtyping relations has been usually provided as the soundness for type safety. The converse direction, the completeness, has been largely ignored in spite […]

13. On-the-Fly Computation of Bisimilarity Distances

Bacci, Giorgio ; Bacci, Giovanni ; Larsen, Kim G. ; Mardare, Radu.
We propose a distance between continuous-time Markov chains (CTMCs) and study the problem of computing it by comparing three different algorithmic methodologies: iterative, linear program, and on-the-fly. In a work presented at FoSSaCS'12, Chen et al. characterized the bisimilarity distance […]

14. An expressive completeness theorem for coalgebraic modal mu-calculi

Enqvist, Sebastian ; Seifan, Fatemeh ; Venema, Yde.
Generalizing standard monadic second-order logic for Kripke models, we introduce monadic second-order logic interpreted over coalgebras for an arbitrary set functor. We then consider invariance under behavioral equivalence of MSO-formulas. More specifically, we investigate whether the […]

15. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes

Chatterjee, Krishnendu ; Křetínská, Zuzana ; Křetínský, Jan.
We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize […]

16. Deriving Probability Density Functions from Probabilistic Functional Programs

Bhat, Sooraj ; Borgström, Johannes ; Gordon, Andrew D. ; Russo, Claudio.
The probability density function of a probability distribution is a fundamental concept in probability theory and a key ingredient in various widely used machine learning methods. However, the necessary framework for compiling probabilistic functional programs to density functions has only recently […]