LCC 2004

Sixth International Workshop on
Logic and Computational Complexity
(formerly, Implicit Computational Complexity)

12 - 13 July 2004   •   Turku, Finland

The Logic and Computational Complexity Workshop (LCC'04) will be a satellite workshop of both the 31st International Colloquium on Automata, Languages and Programming (ICALP'04) and the Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2004).

REGISTRATION

The registration pages for ICALP, LICS, LCC, and all other ICALP-LICS workshops can be found here.

ABSTRACTS OF TALKS

Patrick Baillot   (University of Paris 13)
Type inference for Light Affine Logic Via Constraints on Words

Linear logic provides an approach to implicit computational complexity in the proofs-as-programs paradigm: different variants of this logic, corresponding to different disciplines for duplication, characterize the classes of elementary recursive functions, deterministic (resp., non-deterministic) polynomial time functions. In this talk we will focus on Light Affine Logic (LAL), a system due to Girard-Asperti which corresponds to the class P.

LAL can be seen as a type system for lambda-calculus which refines system F and which guarantees that a well-typed program (with a suitable type) can be executed in polynomial time on any input. Thus it gives a type-based approach to certifying that a lambda-term represents a P function. Additionally the type derivation provides the necessary information about how to execute the term with the polynomial bound. We will discuss the problem of type inference for lambda-terms in LAL and show that this problem is decidable for propositional (quantifier free) LAL. For that we will use explicit subtyping and a reduction to a satisfiability problem for systems of inequations on words over a binary alphabet.

Andrei Bulatov   (University of Oxford)
Polymorphisms of Relational Structures

Many interesting and important properties of relational structures can be expressed using polymorphisms, that is operations on the universe of a relational structure compatible with the relations of the structure. Originally, polymorphisms were used in the study of the complexity of the homomorphism problem, known also as the constraint satisfaction problem or CSP. Later they have proved to be a powerful tool for investigating various problems related to the CSP such as the constraint counting and constraint optimization problems, the quantified CSP, and also for many other problems such as the learnabity of certain classes of formulas, propositional circumscription, etc.

The aim of the talk is to demonstrate how polymorphisms work, to survey various concepts of polymorphisms and types of properties of relational structures they capture, and to survey recent developments in the area.

Stephen Cook   (University of Toronto)
Making Sense of Bounded Arithmetic

We present a unified treatment of logical theories for each of the major complexity classes between AC0 and P, and give simple translations into the quantified propositional calculus.

Victor Dalmau   (Universitat Pompeu Fabra)
The Complexity of Retraction Problems

Let B be a relational structure. The Retraction problem Ret(B) is the problem of deciding given a relational structure A that contains B as a substructure, whether there exists an homomophism from A to B that fixes all the elements in the universe of B.

In this talk we will give an overview of recent results on the complexity and definability of Retraction problems.

Phokion G. Kolaitis   (University of California, Santa Cruz)
Data Exchange: Aspects of Logic and Complexity

Data exchange is the problem of translating data structured under a source database schema to data structured under a target database schema according to a certain specification given by constraints expressed in some logical formalism. Data exchange is an old but recurrent problem in database systems that has taken a new significance in view of the growing need to exchange data across heterogeneous sites.

The aim of this talk is to present an overview of recent results about foundational and algorithmic issues in data exchange such as the semantics of data exchange and the computational complexity of query answering in the context of data exchange. This is joint work with Ron Fagin (IBM Almaden), Renee J. Miller (University of Toronto), and Lucian Popa (IBM Almaden).

Daniel Leivant   (Indiana University Bloomington)
Implicit Complexity Via Logics of Programs

Jean-Yves Marion   (LORIA Nancy)
Resource Analysis by Quasi-Interpretations

We present a survey on methods to analyze program complexity, based on termination orderings and quasi-interpretations. These methods can be implemented to certify the runtime (or memory, stack size) of programs. This topic has some relations with the theory of algorithms as we shall try to explain it. This is a joint work with Guillaume Bonfante and Jean-Yves Moyen (LORIA).

James Royer   (Syracuse University)
Adventures in Time and Space

We investigate type systems, programming formalisms, and compositional semantics that are complexity-theoretically motivated. Our core result is that one can impose one of these type systems on a call-by-value version of PCF and obtain a programming formalism that computes precisely the polynomial-time computable functions at type-level 1, and Kapron and Cook's basic feasible functionals at type-level 2. (This paper considers only type levels 0, 1, and 2.) The type system consists of two parts. The first part, motivated by Bellantoni and Cook's and Leivant's type-theoretic characterizations of polynomial-time, controls space. The second part, motivated by linear typing schemes (particularly Barber and Plotkin's DILL), adds constraints that control time.

Kazushige Terui   (National Institute of Informatics)
Decomposition of Computation via Linear Logic

Linear logic decomposes classical and intuitionistic logics into three components, and the proofs-as-programs interpretation gives each a distinct meaning in terms of computation:

Multiplicatives	=  circuit-like finite computation
Additives	=  nondeterminism
(Generic) Exponentials	=  uniformity

In this talk, we will illustrate these three elements of computation and give characterizations in terms of computational complexity.

Program Co-Chairs

• Martin Grohe (Humboldt-Universität, Berlin)
• Neil Jones (University of Copenhagen)

Steering committee

• Robert Constable (Cornell University)
• Anuj Dawar (University of Cambridge)
• Fernando Ferreira (University of Lisbon)
• Martin Hofmann (Ludwig-Maximilians-Universität München)
• Neil Jones (University of Copenhagen)
• Daniel Leivant (Indiana University Bloomington)
• Jean-Yves Marion (LORIA Nancy)
• Luke Ong (University of Oxford)
• James Royer (Syracuse University), chair
• Helmut Schwichtenberg (Ludwig-Maximilians-Universität München)

WWW-pages

LCC home page:	http://www.cis.syr.edu/~royer/lcc/
ICALP-LICS 2004
main meetings schedules:	http://www.math.utu.fi/ICALP04/schedule.html
workshops schedules:	http://www.math.utu.fi/ICALP04/workshops.html

Contact information

James Royer
Dept. of Elec. Engrg. and Computer Science
Syracuse University
Syracuse, NY 13244, USA
tel: +1 315 443 1028
fax: +1 315 443 1122