Volume 13, Issue 2

2017


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 […]