LICS on Tuesday

Detailed program
Tuesday July 23rd, 2002
See also the unified by-slot program

Sessions take place in auditorium 1 unless otherwise indicated.

Session 5

Chair: Furio Honsell

09:00-09:30  Jens Palsberg, Purdue U, USA
Tian Zhao, Purdue U, USA
Efficient type inference for record concatenation and subtyping
Record concatenation, multiple inheritance, and multiple-object cloning are closely related and part of various language designs. For example, in Cardelli's untyped Obliq language, a new object can be constructed from several existing objects by cloning followed by concatenation; an error is given in case of field name conflicts. Type systems for record concatenation have been studied by Wand, Harper and Pierce, Remy, and others; and type inference for the combination of record concatenation and subtyping has been studied by Sulzmann and by Pottier. In this paper we present the first polynomial-time type inference algorithm for record concatenation, subtyping, and recursive types. Our example language is the Abadi-Cardelli object calculus extended with a concatenation operator. The type inference algorithm runs in O(n5) time where n is the size of the program. Our algorithm enables efficient type checking of Obliq programs without changing the programs at all.

09:30-10:00  Alain Frisch, ENS Paris, France
Giuseppe Castagna, ENS Paris, France
Véronique Benzaken, U Paris XI (Paris-Sud), France
Semantic subtyping
Usually subtyping relations are defined either syntactically by a formal system or semantically by an interpretation of types in an untyped denotational model. In this work we show how to define a subtyping relation semantically, for a language whose operational semantics is driven by types; we consider a rich type algebra, with product, arrow, recursive, intersection, union and complement types. Our approach is to "bootstrap" the subtyping relation through a notion of set-theoretic model of the type algebra. The advantages of the semantic approach are manifold. Foremost we get "for free" many properties (e.g., the transitivity of subtyping) that, with axiomatized subtyping, would require tedious and error prone proofs. Equally important is that the semantic approach allows one to derive complete algorithms for the subtyping relation or the propagation of types through patterns. As the subtyping relation has a natural (inasmuch as semantic) interpretation, the type system can give informative error messages when static type-checking fails. Last but not least the approach has an immediate impact in the definition and the implementation of languages manipulating XML documents, as this was our original motivation.

10:00-10:30  Marcelo Fiore, U Cambridge, UK
Roberto Di Cosmo, U Paris VII, France
Vincent Balat, U Paris VII, France
Remarks on isomorphisms in typed lambda calculi with empty and sum types
Tarski asked whether the arithmetic identities taught in high school are complete for showing all arithmetic equations valid for the natural numbers. The answer to this question for the language of arithmetic expressions using a constant for the number one and the operations of product and exponentiation is affirmative, and the complete equational theory also characterises isomorphism in the typed lambda calculus, where the constant for one and the operations of product and exponentiation respectively correspond to the unit type and the product and arrow type constructors. This paper studies isomorphisms in typed lambda calculi with empty and sum types from this viewpoint. We close an open problem by establishing that the theory of type isomorphisms in the presence of product, arrow, and sum types (with or without the unit type) is not finitely axiomatisable. Further, we observe that for type theories with arrow, empty and sum types the correspondence between isomorphism and arithmetic equality generally breaks down, but that it still holds in some particular cases including that of type isomorphism with the empty type and equality with zero.

Session 6

Chair: Prakash Panangaden

11:00-11:30  Richard Statman, Carnegie Mellon U, USA
On the lambda Y calculus
We show that the word problem for the lambda Y calculus is undecidable and related results.

11:30-12:00  Marco Faella, U Salerno, Italy
Salvatore La Torre, U Salerno, Italy
Aniello Murano, U Salerno, Italy
Dense real-time games
The rapid development of complex and safety-critical systems requires the use of reliable verification methods and tools for system design (synthesis). Many systems of interest are reactive, in the sense that their behavior depends on the interaction with the environment. A natural framework to model them is a two-player game: the system versus the environment. In this context, the central problem is to determine the existence of a winning strategy according to a given winning condition.
We focus on real-time systems, and choose to model the related game as a nondeterministic timed automaton. We express winning conditions by formulas of the branching-time temporal logic TCTL. While timed games have been studied in the literature, timed games with dense-time winning conditions constitute a new research topic.
The main result of this paper is an exponential-time algorithm to check for the existence of a winning strategy for TCTL games where equality is not allowed in the timing constraints. Our approach consists on translating to timed tree automata both the game graph and the winning condition, thus reducing the considered decision problem to the emptiness problem for this class of automata. The proposed algorithm matches the known lower bound on timed games. Moreover, if we relax the limitation we have placed on the timing constraints, the problem becomes undecidable.

12:00-12:30  Catalin Dima, IMAG Grenoble, France
Computing reachability relations in timed automata
We give an algorithmic calculus of the reachability relations on clock values defined by timed automata. Our approach is a modular one, by computing unions, compositions and reflexive-transitive closure (star) of "atomic" relations. The essential tool is a new representation technique for n-clock relations - the 2n-automata - and our strategy is to show the closure under union, concatenation and star of the class of 2n-automata that represent reachability relations in timed automata.

Session 7

Chair: Andrei Voronkov

14:00-15:00  Georg Gottlob, Vienna U of Techn., Austria
Invited lecture: Monadic Queries over Tree-Structured Data

15:00-15:30  Michael Benedikt, Bell Labs, USA
Leonid Libkin, U Toronto, Canada
Tree extension algebras: Logics, automata, and query languages
We study relations on trees defined by first-order constraints over a vocabulary that includes the tree extension relation T<T', holding if and only if every branch of T extends to a branch of T', unary node-tests, and a binary relation checking if the domains of two trees are equal. We show that from such a formula one can generate a tree automaton that accepts the set of tuples of trees defined by the formula, and conversely that every automaton over tree-tuples is captured by such a formula. We look at the fragment with only extension inequalities and leaf tests, and show that it corresponds to a new class of automata on tree tuples, which is strictly weaker then general tree-tuple automata. We use the automata representations to show separation and expressibility results for formulae in the logic. We then turn to relational calculi over the logic defined here: that is, from constraints we extend to queries that have second-order parameters for a finite set of tree tuples. We give normal forms for queries, and use these to get bounds on the data complexity of query evaluation, showing that while general query evaluation is unbounded within the polynomial hierarchy, generic query evaluation has very low complexity, giving strong bounds on the expressive power of relational calculi with tree extension constraints. We also give normal forms for safe queries in the calculus.

Session 8

Chair: Johann Makowsky

16:00-16:30  Markus Frick, U Edinburgh, UK
Martin Grohe, U Edinburgh, UK
The complexity of first-order and monadic second-order logic revisited
The model-checking problem for a logic L on a class C of structures asks whether a given L-sentence holds in a given structure in C. In this paper, we give super-exponential lower bounds for fixed-parameter tractable model-checking problems for first-order and monadic second-order logic.
We show that unless PTIME = NP, the model-checking problem for monadic second-order logic on finite words is not solvable in time f(k)p(n), for any elementary function f and any polynomial p. Here k denotes the size of the input sentence and n the size of the input word. We prove the same result for first-order logic under a stronger complexity theoretic assumption from parameterized complexity theory.
Furthermore, we prove that the model-checking problems for first-order logic on structures of degree 2 and of bounded degree d greater or equal 3 are not solvable in time 22o(k)p(n) (for degree 2) and 222o(k)p(n) (for degree d), for any polynomial p, again under an assumption from parameterized complexity theory. We match these lower bounds by corresponding upper bounds.

16:30-17:00  Jean-Marie Le Bars, U Caen, France
The 0-1 law fails for frame satisfiability of propositional modal logic
The digraph property KERNEL is a very simple and well-known property studied in various areas. We previously defined a variant of this property as a counterexample of 0-1 law for the monadic existential second order logic with at most two first-order variables, over structures with 16 binary relations. Goranko and Kapron have defined two variants in frames which expresses frame satisfiability of propositional modal logic, also expressible in a small fragment of the logic above over structures with only one relation.
We propose another variant of KERNEL which provides a counterexample of the 0-1 law for frame satisfiability of propositional modal logic. This refutes a result by Halpern and Kapron which establishes that the 0-1 law holds for this logic. It also strongly refines our previous counterexample.

17:00-17:30  Hajime Ishihara, Japan Advanced Inst. of Science and Techn., Japan
Bakhadyr Khoussainov, U Auckland, New Zealand
Sasha Rubin, U Auckland, New Zealand
Some results on automatic structures
We study the class of countable structures which can be presented by synchronous finite automata. We reduce the problem of existence of an automatic presentation of a structure to that for a graph. We exhibit a series of properties of automatic equivalence structures, linearly ordered sets and permutation structures. These serve as a first step in producing practical descriptions of some automatic structures or illuminating the complexity of doing so for others.

Conference dinner

Joint with FME, RTA
Room: Restaurant Luftkastellet

19:30-21:30  Banquet

21:30-22:30  Martin Davis, U California-Berkeley, USA
Plenary talk: Alan Turing & the advent of the computer