 | |
Sessions
take place in auditorium 1 unless otherwise indicated.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. |
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. |
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. |
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. |
Joint
with FME, RTA
Room:
Restaurant Luftkastellet | 21:30- | 22:30
| Martin Davis, U
California-Berkeley, USA
Plenary
talk: Alan Turing & the advent of the
computer |
| |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
