LCC'17 MEETING
The Eighteenth International Workshop on Logic and Computational Complexity
will be held in Reykjavik, Iceland, on June 19, 2017,
as an affiliated meeting of
LiCS 2017
.
LCC meetings are aimed at the foundational interconnections between
logic and computational complexity, as present, for example, in
implicit computational complexity (descriptive and typetheoretic methods);
deductive formalisms as they relate to complexity (e.g. ramification,
weak comprehension, bounded arithmetic, linear logic and resource logics);
complexity aspects of finite model theory and databases;
complexitymindful program derivation and verification;
computational complexity at higher type; and proof complexity.
The program will consist of invited
lectures as well as contributed papers selected by the Program Committee.
IMPORTANT DATES
Paper submission deadline: 
April 14, 2017 
Authors' notification: 
May 1, 2017 
Workshop: 
June 19, 2017 
INVITED SPEAKERS
 Arnaud Durand, Université Denis Diderot  Paris 7
 Damiano Mazza, CNRSUniversité ParisNord
PROGRAM
 08:5509:00
 Welcome.
 09:0010:00  Invited talk



Church meets Cook and Levin
Damiano Mazza (CNRSUniversité ParisNord)
The CookLevin theorem (the statement that SAT is NPcomplete) is a central
result in structural complexity theory. What would a proof of the CookLevin
theorem look like if the reference model of computation were not Turing
machines but the lambdacalculus? We will see that exploring the alternative
universe of "structural complexity with lambdaterms instead of Turing
machines" brings up a series of interesting questions, both technical and
philosophical. Some of these have satisfactory answers, leading us in
particular to a proof of the CookLevin theorem using tools of prooftheoretic
and semantic origin (linear logic, Scott continuity), but many others are fully
open, leaving us wondering about the interactions (or lack thereof) between
complexity theory and proof theory/programming languages theory.
 10:0010:25  Coffee break

 Session I: Programs and proofs

 10:2510:50

Analyzing probabilistic programs with dynamic logic
Tong Cheng (Huazhong University of Science and Technology)
We present a unified framework for the analysis of probabilistic programs based
on Dynamic Logic in which both iterative and recursive programs can be
analyzed. We augment the traditional rules of probabilistic Dynamic Logic with
rules for assignment based on schematic Kleene algebra, as well as proof rules
for recursive programs with callbyvalue parameters. We show soundness of our
system with respect to the standard Markov kernel semantics. We give an example
of their use in the analysis of the Coupon Collector’s Problem.
 10:5011:15

Proof complexity and proof compression via combinatorial flows
Lutz Strassburger (INRIA Saclay  IledeFrance)
Combinatorial flows are a novel way of representing proofs in a "syntaxfree"
way that also includes cut and substitution as proof compression mechanisms. In
this paper we show how combinatorial flows are translated into syntactic proofs
and vice versa, establishing that combinatorial flows are pequivalent to Frege
systems with substitution.
 11:1512:25  Break

 Session II: Complexity of logical calculi

 11:2511:50

Discrete temporal constraint satisfaction problems
Manuel Bodirsky (TU Desden), Barnaby Martin (Durham University), Antoine Mottet (Institut fűr Algebra, TU Dresden)
A discrete temporal constraint satisfaction problem is a constraint
satisfaction problem (CSP) whose constraint language consists of relations that
are firstorder definable over the order of the integers. We prove that every
discrete temporal CSP is in P, NPcomplete, can be formulated as a finite
domain CSP.
 11:5012:15

Filtration versus team semantics
Martin Lück (Leibniz Universität Hannover)
Modal Team Logic (MTL) extends Väänänen's Modal Dependence Logic (MDL) by
Boolean negation. Its satisfiability problem is decidable, but the exact
complexity is not yet understood very well. We investigate a modeltheoretical
approach and generalize the successful filtration technique to work in team
semantics. We identify an "existential" fragment of MTL that enjoys the
exponential model property and is therefore, like Propositional Team Logic
(PTL), complete for the class AEXPTIME(poly). Moreover, superexponential
filtration lower bounds for different fragments of MTL are proven, up to the
full logic having no filtration for any elementary size bound. As a corollary,
superexponential gaps of succinctness between MTL fragments of equal expressive
power are shown.
 12:1513:45  Lunch

 Session III: Definability

 13:4514:10

Slicewise definability in firstorder logic with bounded quantifier rank
Yijia Chen (Fudan University), Jörg Flum (University of Freiburg), and Xuangui Huang (Shanghai Jiao Tong University)
For every $q\in \mathbb N$ let $\textrm{FO}_q$ denote the class of sentences of
firstorder logic FO of quantifier rank at most $q$. If a graph property can be
defined in $\textrm{FO}_q$, then it can be decided in time $O(n^q)$. Thus,
minimizing q has favorable algorithmic consequences. Many graph properties
amount to the existence of a certain set of vertices of size $k$. Usually this
can only be expressed by a sentence of quantifier rank at least $k$. We use the
colorcoding method to demonstrate that some (hyper)graph problems can be
defined in $\textrm{FO}_q$ where $q$ is independent of $k$. This property of a
graph problem is equivalent to the question of whether the corresponding
parameterized problem is in the class $\textrm{paraAC}^0$.
It is crucial for our results that the FOsentences have access to builtin
addition and multiplication. It is known that then FO corresponds to the
circuit complexity class uniform $\textrm{AC}^0$. We explore the connection
between the quantifier rank of FOsentences and the depth of
$\textrm{AC}^0$circuits, and prove that $\textrm{FO}_q \subsetneq
\textrm{FO}_{q+1}$ for structures with builtin addition and multiplication.
 14:1014:35

A complexity theory for implicit graph representations
Maurice Chandoo (Leibniz Universität Hannover)
In an implicit graph representation the vertices of a graph are assigned short
labels such that adjacency of two vertices can be algorithmically determined
from their labels. This allows for a spaceefficient representation of graph
classes that have asymptotically fewer graphs than the class of all graphs such
as forests or planar graphs. A fundamental question is whether every smaller
graph class has such a representation. We consider how restricting the
computational complexity of such representations affects what graph classes can
be represented. A formal language can be seen as implicit graph representation
and therefore complexity classes such as P or NP can be understood as set of
graph classes. We investigate this complexity landscape and introduce
complexity classes defined in terms of first order logic that capture
surprisingly many of the graph classes for which an implicit representation is
known. Additionally, we provide a notion of reduction between graph classes
which reveals that trees and interval graphs are complete for certain fragments
of first order logic in this setting.
 14:3514:45  Break

 14:4515:45  Invited talk



A survey on descriptive and implicit characterizations of small complexity
classes (invited talk)
Arnaud Durand (Université Denis Diderot  Paris 7)
Descriptive and implicit complexities talk about computational complexity
without machines. They offer a logical and algebraic point of view on
computational resources that have proved to be fruitful in domain such as
database or programming theory.
In this talk, we will survey some methods used to characterize small complexity
classes, from the early result of Cobham for polynomial time to more recent
ones for circuit classes. We will also consider the more general problem of
capturing counting complexity classes and present some new results.
 15:4516:10  Coffee break

 Session IV: Descriptive complexity and deductive formalisms

 16:1016:35

Characterizing circuit complexity classes by logics with recursion
Anselm Haak (Leibniz Universität Hannover)
We introduce a certain kind of recursion scheme into firstorder variants of
which allow us to capture a number of classes from circuit complexity, nameley
AC^{1}, SAC^{1}, NC^{1}
as well as their counting analogues. The advantage of our new
approach is that it allows for a unified characterization of multiple important
classes.
 16:3517:00

Symmetric circuits for rank logic
Anuj Dawar (University of Cambridge), Gregory Wilsenach (University of Cambridge)
Anderson and Dawar (2014) showed that fixedpoint logic with counting (FPC) can
be characterised by uniform families of polynomialsize symmetric circuits. We
give a similar characterisation for fixedpoint logic with rank (FPR) by means
of symmetric circuits including rank gates. This analysis requires a
significant extension of previous methods to deal with gates computing Boolean
functions which are not themselves symmetric. In particular, we show that the
support theorem of Anderson and Dawar can be extended to circuits whose gates
satisfy a property that we term "matrixsymmetry".
 17:0017:25

An implicit characterisation of the polynomial hierarchy in an unbounded
arithmetic
Anupam Das (LIP, ENS Lyon), Patrick Baillot (CNRS, ENS Lyon)
We consider extensions of theories based on the BellantoniCook function
algebra for FPTIME by induction principles without bounds on quantifiers.
Instead, we limit quantification to 'safe' arguments and show that the provably
total functions are just those of FPH. Our witness extraction proof relies on
freecut elimination in the logic, making use of the witness function method,
due to Buss, rather than realisability and Dialectica approaches more common in
implicit complexity. Our results closely resemble analogous ones from bounded
arithmetic, only for an unbounded setting, and the proof generalises those for
previous approaches characterising FPTIME via the BellantoniCook framework. We
present further comparisons to the bounded arithmetic setting and give tiered
arithmetic theories analogous to the S^{i}_{2}
and V^{i} hierarchies of bounded
arithmetic.
PROGRAM CHAIRS
PROGRAM COMMITTEE
SUBMISSION OF PAPERS
We welcome submissions of abstracts based on work submitted or published
elsewhere, provided that all pertinent information is disclosed at
submission time. There will be no formal reviewing as is usually
understood in peerreviewed conferences with published proceedings. The
program committee checks relevance and may provide additional feedback.
Submissions must be in English and in the form of an abstract of about 34
pages. All submissions should be submitted through Easychair at:
https://easychair.org/conferences/?conf=lcc2017
REGISTRATION
See the LiCS registration page.
CONTACT
To contact the workshop organizers, please send email to
lcc2017@easychair.org.
