LCC'15 MEETING
The Sixteenth International Workshop on Logic and Computational Complexity
will be held in Kyoto, Japan, on July 4-5, 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 type-theoretic 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;
complexity-mindful 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 4-5, 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 Polynomial-time Computable Analysis (invited talk)
Akitoshi Kawamura (University of Tokyo)
Abstract: Weihrauch reduction can be seen as an analogue of
many-one reduction for type-two computational problems, and has
been used to classify theorems of the for-all-exists 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 First-Order 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 Sherali-Adams Relaxations for General-valued CSPs
(invited talk)
Stanislav Živný (University of Oxford)
Abstract: In this talk, we will present recent results giving
an algebraic characterisation of general-valued constraint
satisfaction problems that can be solved to optimality using
Sherali-Adams 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 polynomial-time 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
Fraenkel-Mostowski 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 ``orbit-finiteness''. 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 orbit-finiteness. For example, orbit-finite
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 orbit-finite 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 orbit-finite 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 Kripke-Platek set theory
which have the potential to characterise the above classes as
their Sigma-1 definable functions.
- 11:50 - 12:15
- Formalizing Termination Proofs under Polynomial Quasi-interpretations
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
- Lambda-calculus, 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 lambda-calculus (in
collaboration with Dal Lago, Barenbaum & Mazza, and Sacerdoti
Coen).
We will first focus on the weak lambda-calculus, the model
underlying functional programming languages, for which it is
well-known that the number of beta-steps is a reasonable
cost-model. The proofs of such a result rely on alternative
representations of lambda-calculus extended with some form of
sharing, as abstract machines or graphical formalisms. We will
provide an abstract view, using as a tool a lambda-calculus with
explicit sharing, the Linear Substitution Calculus, and
encompassing all main evaluation schemes
(call-by-name/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 proof-assistants, focussing on the recent result
that the number of beta-steps is a reasonable cost-model 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 Lambda-calculus and Implicit Computational Complexity
Damiano Mazza
- 15:30 - 16:00
- break
-
- 4th session
- 16:00 - 16:50
- Information Flow and Complexity (invited talk)
Jean-Yves 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
security-typed 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 data-structures has been central to both
theoretical and practical facets of programming. Then, we
introduced an imperative language with pointers based on
while-loops and recursive function calls The domain of computation
consists of first-order 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, C-structure
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 peer-reviewed 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 3-4
pages. All submissions should be submitted through Easychair at:
https://easychair.org/conferences/?conf=lcc2015
REGISTRATION
See the ICALP/LICS page.
|
