Special Issue for the Conferences on Computer Science Logic and Logic in Computer Sciences (CSL-LICS) 2014

Editors: Thomas A Henzinger, Dale Miller

The Vienna Summer of Logic in July 2014 attracted a great number of researchers working in logic to Vienna. To take advantage of this unprecedented confluence of logicians, especially those working in computational logic, the organizers of the CSL and LICS series of meetings decided to merge the 2014 editions of these meetings into one meeting titled the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). This joint meeting had one program committee, one program, and one proceedings.

A small number of papers from the proceedings were selected and their authors were invited to submit a full version of their paper to this special issue. All submissions were refereed according to the usual standards of LMCS with each paper being reviewed by three experts in the field. We are grateful to the authors for their excellent submissions and to the reviewers for their efforts to evaluate and improve these papers.

Thomas A. Henzinger and Dale Miller
CSL-LICS 2014, Program Committee Chairs

1. Preservation and decomposition theorems for bounded degree structures

Harwath, Frederik ; Heimberg, Lucas ; Schweikardt, Nicole.
We provide elementary algorithms for two preservation theorems for first-order sentences (FO) on the class \^ad of all finite structures of degree at most d: For each FO-sentence that is preserved under extensions (homomorphisms) on \^ad, a \^ad-equivalent existential […]

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

4. On the characterization of models of H*: The semantical aspect

Breuvart, Flavien.
We give a characterization, with respect to a large class of models of untyped lambda-calculus, of those models that are fully abstract for head-normalization, i.e., whose equational theory is H* (observations for head normalization). An extensional K-model $D$ is fully abstract if and only if it is […]