LCC'15 MEETING
The Sixteenth International Workshop on Logic and Computational Complexity
will be held in Kyoto, Japan, on July 45, as an affiliated meeting of
ICALP/LICS
2015.
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 29, 2015 (extended)

Authors' notification:
 May 14, 2015

Workshop:
 July 45, 2015

INVITED SPEAKERS
PROGRAM
4th (Sat)

 1st session
 09:30  10:30
 Proof Complexity of Quantified Boolean Formulas (invited talk)
Olaf Beyersdorff (University of Leeds)
Abstract: The main aim in proof complexity is to understand
the complexity of theorem proving. Arguably, what is even more
important is to establish techniques for lower bounds, and the
recent history of computational complexity speaks volumes on how
difficult it is to develop general lower bound
techniques. Understanding the size of proofs is important for at
least two reasons. The first is its tight relation to the
separation of complexity classes: NP vs. coNP for propositional
proofs, and NP vs. PSPACE in the case of proof systems for
quantified boolean formulas (QBF). The second reason to study
lower bounds for proofs is the analysis of SAT and QBF solvers:
powerful algorithms that efficiently solve the classically hard
problems of SAT and QBF for large classes of practically relevant
formulas.
 10:30  11:00
 break

 2nd session
 11:00  11:50
 Weihrauch Reducibility in Polynomialtime Computable Analysis (invited talk)
Akitoshi Kawamura (University of Tokyo)
Abstract: Weihrauch reduction can be seen as an analogue of
manyone reduction for typetwo computational problems, and has
been used to classify theorems of the forallexists form
involving real numbers and other continuous data. With some care,
such reducibility argument can be applied to settings with limited
resources such as polynomial time. In this talk, I will introduce
some of such reducibility and completeness results.
 11:50  12:15
 On Finite Domains in FirstOrder Linear Temporal Logic
Julien Brunel, David Chemouil and Denis Kuperberg
 12:15  12:40
 A Circuit Complexity Approach to Transductions
Michaël Cadilhac, Andreas Krebs, Michael Ludwig and Charles
Paperman
 12:40  14:00
 lunch break

 3rd session
 14:00  14:50
 The Power of SheraliAdams Relaxations for Generalvalued CSPs
(invited talk)
Stanislav Živný (University of Oxford)
Abstract: In this talk, we will present recent results giving
an algebraic characterisation of generalvalued constraint
satisfaction problems that can be solved to optimality using
SheraliAdams relaxations. We will also show several consequences
of this characterisation, including algorithmic results and
complexity classifications of various optimisation problems.
 14:50  15:15
 A Definability Dichotomy for Finite Valued CSPs
Anuj Dawar and Pengming Wang
 15:30  16:00
 break

 4th session
 16:00  16:50
 Computability and Complexity of Conditioning and Conditional Independence (invited talk)
Cameron Freer (MIT, Massachusetts)
Abstract: We examine two fundamental aspects of probability
theory through the lens of computability and computational
complexity. The formation of conditional distributions is a key
operation in machine learning and nonparametric Bayesian
statistics. The conditional independence that follows from various
symmetry properties such as exchangeability plays an important
role in the analysis of sequential and relational data. We present
background on and results for several problems in these settings,
in both computable and polynomialtime computable variants. Joint
work with Ackerman, Avigad, Roy, and Rute.
 16:50  17:15
 Consistency Proof of a Feasible Arithmetic Inside a Bounded Arithmetic
Yoriyuki Yamagata
 17:15  17:40
 On the Satisfiability Problem for Classes of Structures Related to
Finite Dimensional Vector Spaces
Christian Herrmann, Yasuyuki Tsukamoto and Martin Ziegler
5th (Sun)

 1st session
 09:30  10:30
 Computation with Atoms (invited talk)
Mikołaj Bojańczyk (Warsaw University)
Abstract: Sets with atoms (also known as permutation models, or
FraenkelMostowski sets) were introduced in set theory by Fraenkel
in 1922, and further developed by Mostowski. In 1999, they were
rediscovered for computer science by the semantics community, where they
are called nominal sets. This talk is about a research programme, which
studies a notion of finiteness which only makes sense in sets with atoms,
called ``orbitfiniteness''. The research programme is to see what happens
to notions from computer science when sets are replaced by sets with atoms,
and finiteness is replaced by orbitfiniteness. For example, orbitfinite
automata turn out to be the same thing as automata with registers on data
words. The general idea is that many algorithms still work, while covering
a wider variety of inputs (in the example of orbitfinite automata, the
standard emptiness and minimisation algorithms work, but the
determinisation algorithm fails). Another theme is that the wider class of
structures requires seeing new (and perhaps surprising) connections, e.g.
the study of orbitfinite Turing machines naturally leads to the algebraic
theory constraint satisfaction problems and to finite model theory.
 10:30  11:00
 break

 2nd session
 11:00  11:15
 Feasible Computable Set Functions (invited talk)
Arnold Beckmann (Swansea University)
Abstract: Recently, various restrictions of the primitive
recursive set functions have been proposed with the aim to capture
feasible computation on sets. Amongst these are the "Safe
Recursive Set Functions" (Beckmann, Buss, Friedman, accepted for
publication in JSL) the "Predicatively Computable Set Functions"
(Arai, Archive for Mathematical Logic, vol. 54 (2015),
pp. 471–485) and the "Cobham Recursive Set Functions" (Beckmann,
Buss, Friedman, Müller, Thapen, in progress).
In my talk, I will review the definition of the above classes, and
present an overview of the results characterising the functions
representable by them. Time permitted, I will speak about recent
developments on defining restrictions of KripkePlatek set theory
which have the potential to characterise the above classes as
their Sigma1 definable functions.
 11:50  12:15
 Formalizing Termination Proofs under Polynomial Quasiinterpretations
Naohi Eguchi
 12:15  12:40
 Bounded Arithmetic for Monotone and Deep Inference Systems
Anupam Das
 12:40  14:00
 lunch break

 3rd session
 14:00  14:50
 Lambdacalculus, Sharing, and Time Cost Models (invited talk)
Beniamino Accattoli (INRIA, Palaiseau)
Abstract: This talk will survey recent works about the
understanding of time cost models for lambdacalculus (in
collaboration with Dal Lago, Barenbaum & Mazza, and Sacerdoti
Coen).
We will first focus on the weak lambdacalculus, the model
underlying functional programming languages, for which it is
wellknown that the number of betasteps is a reasonable
costmodel. The proofs of such a result rely on alternative
representations of lambdacalculus extended with some form of
sharing, as abstract machines or graphical formalisms. We will
provide an abstract view, using as a tool a lambdacalculus with
explicit sharing, the Linear Substitution Calculus, and
encompassing all main evaluation schemes
(callbyname/value/need). First, we will discuss the overhead due
to sharing itself, and then the overhead of implementing it via an
abstract machine.
The second part of the talk will discuss strong reduction, the
model underlying proofassistants, focussing on the recent result
that the number of betasteps is a reasonable costmodel also in
this case. We will explain why an additional layer of sharing,
called useful sharing, is required, and then we will reconsider
sharing and abstract machines overheads in this new setting.
 14:50  15:15
 The Parsimonious Lambdacalculus and Implicit Computational Complexity
Damiano Mazza
 15:30  16:00
 break

 4th session
 16:00  16:50
 Information Flow and Complexity (invited talk)
JeanYves Marion (LORIA, Nancy)
Abstract: In 2011, we proposed a type system for a small
imperative programming language, which certifies time bounds. The
starting point is the observation that there is a link between
securitytyped languages and the tiering mechanism implied in
complexity analysis.This result has been extended to concurrent
programming paradigms. Another important feature is the data
structure on which the computation is run. The interplay of
algorithms and datastructures has been central to both
theoretical and practical facets of programming. Then, we
introduced an imperative language with pointers based on
whileloops and recursive function calls The domain of computation
consists of firstorder structures like in Hofmann and Schopp
(2010). However here, structures may evolve during a
computation. For this, there are a new and a free operation. As a
result, the data structure is closed to records, Cstructure
construction or to objects. We establish a characterization of the
class of all functions computable in polynomial time. I also gave
a characterization of Logspace. The difference with other
approaches is that the underlying computational model is inspired
by reference machines like Kolmogorov & Uspensky machines,
Schonhage storage modification machines and Gurevich abstract
state machines.
 16:50  17:15
 Models of Bounded Arithmetic by Restricted Reduced Powers
Michal Garlik
 17:15  17:40
 Focusing Light Logics
Alexis Saurin
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=lcc2015
REGISTRATION
See the ICALP/LICS page.
