Selected Papers of the joint International Conferences on "Rewriting Techniques and Applications" and "Typed Lambda Calculi and Applications" RTA/TLCA 2014

Editor: Gilles Dowek

This special issue of Logical Methods in Computer Science presents a selection of papers presented at the joint *25th International Conference on Rewriting Techniques and Applications* and *12th International Conference on Typed Lambda Calculi and Applications* held in July 2014 in Vienna. This conference aimed at bringing together researchers working on rewriting, lambda-calculus, and strongly related topics such as proof theory. The two conferences have now merged into the conference *Formal Structures for Computation and Deduction*.

The two papers published in this special issue have been reviewed using the standard review mechanism of LMCS. They illustrate the diversity of the questions discussed during this meeting, ranging from the proof theory for non deterministic languages to the models of lambda calculus, through the complexity of unification.

Gilles Dowek
RTA-TLCA 2014 Program chair

1. Unification and Logarithmic Space

Clément Aubert ; Marc Bagnol.

We present an algebraic characterization of the complexity classes Logspace and Nlogspace, using an algebra with a composition law based on unification. This new bridge between unification and complexity classes is rooted in proof theory and more specifically linear logic and geometry of interaction. We show how to build a model of computation in the unification algebra and then, by means of a syntactic representation of finite permutations in the algebra, we prove that whether an observation (the algebraic counterpart of a program) accepts a word can be decided within logarithmic space. Finally, we show that the construction naturally corresponds to pointer machines, a convenient way of understanding logarithmic space computation.

2. All-Path Reachability Logic

Andrei Stefanescu ; Stefan Ciobaca ; Radu Mereuta ; Brandon Moore ; Traian Florin Serbanuta ; Grigore Rosu.

This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g., concurrent) languages, referred to as all-path reachability logic. It derives partial-correctness properties with all-path semantics (a state satisfying a given precondition reaches states satisfying a given postcondition on all terminating execution paths). The proof system takes as axioms any unconditional operational semantics, and is sound (partially correct) and (relatively) complete, independent of the object language. The soundness has also been mechanized in Coq. This approach is implemented in a tool for semantics-based verification as part of the K framework (http://kframework.org)