Logic and Computational Complexity

An International Workshop Series


 

Home

Steering-Com

Past-meetings

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.