Volume 12, Issue 1


1. Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion

Debois, Søren ; Hildebrandt, Thomas ; Slaats, Tijs ; Yoshida, Nobuko.
We present the first session typing system guaranteeing request-response liveness properties for possibly non-terminating communicating processes. The types augment the branch and select types of the standard binary session types with a set of required responses, indicating that whenever a […]

2. Proof equivalence in MLL is PSPACE-complete

Heijltjes, Willem ; Houston, Robin.
MLL proof equivalence is the problem of deciding whether two proofs in multiplicative linear logic are related by a series of inference permutations. It is also known as the word problem for star-autonomous categories. Previous work has shown the problem to be equivalent to a rewiring problem on […]

3. Weak topologies for Linear Logic

Kerjean, Marie.
We construct a denotational model of linear logic, whose objects are all the locally convex and separated topological vector spaces endowed with their weak topology. The negation is interpreted as the dual, linear proofs are interpreted as continuous linear functions, and non-linear proofs as […]

4. (Leftmost-Outermost) Beta Reduction is Invariant, Indeed

Accattoli, Beniamino ; Lago, Ugo Dal.
Slot and van Emde Boas' weak invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time. Is lambda-calculus a reasonable machine? Is there a way to measure the computational complexity of a lambda-term? This paper presents the first complete […]

5. Separating Regular Languages with First-Order Logic

Place, Thomas ; Zeitoun, Marc.
Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a first-order definable separator. We prove that in […]

6. Simulation Problems Over One-Counter Nets

Hofman, Piotr ; Lasota, Slawomir ; Mayr, Richard ; Totzke, Patrick.
One-counter nets (OCN) are finite automata equipped with a counter that can store non-negative integer values, and that cannot be tested for zero. Equivalently, these are exactly 1-dimensional vector addition systems with states. We show that both strong and weak simulation preorder on OCN […]

7. History-Register Automata

Grigore, Radu ; Tzevelekos, Nikos.
Programs with dynamic allocation are able to create and use an unbounded number of fresh resources, such as references, objects, files, etc. We propose History-Register Automata (HRA), a new automata-theoretic formalism for modelling such programs. HRAs extend the expressiveness of previous […]

8. A Sorted Semantic Framework for Applied Process Calculi

Borgström, Johannes ; Gutkovas, Ramūnas ; Parrow, Joachim ; Victor, Björn ; Pohjola, Johannes Åman.
Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies. Several such formalisms, e.g. the applied pi calculus, […]

9. Order-Invariant Types and Their Applications

Barcelo, Pablo ; Libkin, Leonid.
Our goal is to show that the standard model-theoretic concept of types can be applied in the study of order-invariant properties, i.e., properties definable in a logic in the presence of an auxiliary order relation, but not actually dependent on that order relation. This is somewhat surprising […]