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).
|All talks will be in Room 2 of the Pharma City building.|
|MONDAY MORNING, JULY 12|
|09:00-10:00||Stephen Cook||Making Sense of Bounded Arithmetic|
|10:00-11:00||Victor Dalmau||The Complexity of Retraction Problems|
|11:00-11:30||Coffee||11:30-12:30||Andrei Bulatov||Polymorphisms of Relational Structures|
|MONDAY AFTERNOON, JULY 12|
|14:00-15:00||Phokion Kolaitis||Data Exchange: Aspects of Logic and Complexity|
|15:00-16:00||Patrick Baillot||Type Inference for Light Affine Logic Via Constraints on Words|
|16:00-16:30||Coffee||16:30-17:30||Jean-Yves Marion||Resource Analysis by Quasi-Interpretations|
|TUESDAY MORNING, JULY 13|
|09:00-10:00||Daniel Leivant||Implicit Complexity Via Logics of Programs|
|10:00-11:00||Kazushige Terui||Decomposition of Computation Via Linear Logic|
|11:00-11:30||Coffee||11:30-12:30||James Royer||Adventures in Time and Space|
The registration pages for ICALP, LICS, LCC, and all other ICALP-LICS workshops can be found here.
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 StructuresMany 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 ArithmeticWe 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 ProblemsLet 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 ComplexityData 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-InterpretationsWe 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 SpaceWe 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 LogicLinear logic decomposes classical and intuitionistic logics into three components, and the proofs-as-programs interpretation gives each a distinct meaning in terms of computation:
In this talk, we will illustrate these three elements of computation and give characterizations in terms of computational complexity.
Multiplicatives = circuit-like finite computation Additives = nondeterminism (Generic) Exponentials = uniformity
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
Dept. of Elec. Engrg. and Computer Science
Syracuse, NY 13244, USA
+1 315 443 1028
+1 315 443 1122