SUNDAY 29 JUNE
08:30-09:30 Invited Speaker
(Chair: Andrew Pitts)
Luca Cardelli (DEC):
A Theory of Objects.
09:30-10:00 Coffee break
10:00-12:00 Rewriting & Deduction
(Chair: Claude Kirchner)
Franz Baader (RWTH Aachen):
Combination of Compatible Reduction Orderings
that are Total on Ground Terms.
Adel Bouhoula (INRIA Lorraine & CRIN),
Jean-Pierre Jouannaud (LRI, CNRS&Université de Paris-Sud):
Automata-Driven Automated Induction.
Hubert Comon & Florent Jacquemard
(LRI, CNRS & Université de Paris-Sud):
Ground Reducibility is EXPTIME-Complete.
Roberto Di Cosmo (DMI-LIENS, Paris) and
Delia Kesner (LRI, CNRS & Université de Paris-Sud):
Strong Normalization of Explicit Substitutions via Cut
Elimination in Proof Nets.
12:00-13:30 Lunch
13:30-15:30 Linear Logic & Game Semantics
(Chair: Pat Lincoln)
Max Kanovich (Russian State Univ. for the Humanities)
Takayasu Ito (Tohoku University):
Temporal Linear Logic Specifications for
Concurrent Processes.
Jim Laird (University of Edinburgh):
Full Abstraction for Functional Languages with Control.
Patrick Baillot (IML-CNRS Marseille),
Vincent Danos (Université Paris 7-CNRS),
Thomas Ehrhard (IML-CNRS Marseille)
Laurent Regnier (IML-CNRS Marseille):
Believe it or not, AJM's Games Model is a Model
of Classical Linear Logic.
Dominic J.D. Hughes (PRG, University of Oxford):
Games and Definability for System F.
15:30-16:00 Coffee break
16:00-17:30 Model Checking
(Chair: Ken McMillan)
Henrik Reif Andersen & Henrik Hulgaard
(Technical University of Denmark):
Boolean Expression Diagrams.
Stefan Dziembowski, Marcin Jurdzinski & Igor Walukiewicz
(Warsaw University):
How Much Memory is Needed to Win Infinite Games?
Michael Huth (Kansas State University) &
Marta Kwiatkowska (University of Birmingham):
Quantitative Analysis and Model Checking.
18:30-19:30 Invited Speaker
(Chair: Moshe Vardi)
Anita Feferman
(Biographer, Independent Scholar, Stanford, CA):
The Saga of Alfred Tarski: From Warszawa to Berkeley
MONDAY 30 JUNE
08:30-10:00 Tutorial
(Chair: David Basin)
David McAllester (AT & T Labs):
Methods of Automated Complexity Analysis for
Inference Rules.
10:00-10:30 Coffee break
10:30-12:00 Concurrency
(Chair: Matthew Hennessy)
Naoki Kobayashi (University of Tokyo):
A Partially Deadlock-Free Typed Process Calculus.
Julian Rathke (University of Sussex):
Unique Fixpoint Induction for Value-Passing Processes.
Richard Blute (University of Ottawa),
Josée Desharnais (McGill University, Montreal),
Abbas Edalat (Imperial College) &
Prakash Panangaden (BRICS, University of Aarhus):
Bisimulation for Labelled Markov Processes.
12:00-13:30 Lunch
13:30-15:30 Temporal Logic & Automata
(Chair: Colin Stirling)
Eugene Asarin (Inst. for Information Transmission
Problems, Moscow),
Paul Caspi (VERIMAG),
Oded Maler (VERIMAG):
A Kleene Theorem for Timed Automata.
David Janin (LaBRI - ENSERB, Université de Bordeaux I):
Automata, Tableaus and a Reduction Theorem for
Fixpoint Calculi in Arbitrary Complete Lattices.
P.S. Thiagarajan (BRICS, University of Aarhus) &
Igor Walukiewicz (Warsaw University):
An Expressively Complete Linear Time Temporal Logic for
Mazurkiewicz Traces.
Dexter Kozen (Cornell University):
On the Complexity of Reasoning in Kleene Algebra.
15:30-16:00 Coffee break
16:00-18.00 Finite Model Theory
(Chair: Anuj Dawar)
Leonid Libkin (Bell Laboratories):
On the Forms of Locality over Finite Models.
Martin Grohe (Albert-Ludwigs-Universität Freiburg):
Large Finite Structures with Few Lk-Types.
Kousha Etessami (BRICS, University of Aarhus),
Moshe Y. Vardi (Rice University) &
Thomas Wilke (Christian-Albrechts-Universität zu Kiel):
First-Order Logic with Two Variables and
Unary Temporal Logic.
Oliver Matz & Wolfgang Thomas (Universität Kiel):
The Monadic Quantifier Alternation Hierarchy over
Graphs is Infinite.
20:00 Business meeting
TUESDAY 1 JULY
08:30-09:30 Invited Speaker
(Chair: Damian Niwinski)
Leszek Pacholski (Instytut Informatyki, Wroclaw):
Set Constraints.
09:30-10:00 Coffee break
10:00-12:00 Semantics & Domain Theory I
(Chair: Stephen Brookes)
Peter John Potts, Abbas Edalat & Martin Hötzel Escardo
(Imperial College, London):
Semantics of Exact Real Arithmetic.
Jon G. Riecke (Bell Laboratories) &
Anders Sandholm (BRICS, University of Aarhus):
A Relational Account of Call-by-Value Sequentiality.
Marcelo Fiore, Gordon Plotkin & John Power
(University of Edinburgh):
Complete Cuboidal Sets in Axiomatic Domain Theory.
Daniele Turi & Gordon Plotkin (University of Edinburgh):
Towards a Mathematical Operational Semantics.
12:00-13:30 Lunch
13:30-15:30 Decidability & Complexity Theory
(Chair: Jan Krajicek)
Sergei Vorobyov (Max-Planck-Institut für Informatik):
The "Hardest" Natural Decidable Theory.
Erich Grädel (RWTH Aachen), Martin Otto (RWTH Aachen) &
Eric Rosen (Technion Haifa):
Two-Variable Logic with Counting is Decidable.
Leszek Pacholski (University of Wroclaw),
Wieslaw Szwast & Lidia Tendera (University of Opole):
Complexity of Two-Variable Logic with Counting.
Guo-Qiang Zhang (University of Georgia) &
William C. Rounds (University of Michigan):
Complexity of Power Default Reasoning.
15:30-16:00 Coffee break
16:00-17:30 Types and Constraints
(Chair: Jens Palsberg)
Nevin Heintze (Bell Laboratories) &
David McAllester (AT & T Labs):
On the Cubic Bottleneck in Subtyping and Flow Analysis.
Fritz Henglein & Jakob Rehof (Copenhagen University):
The Complexity of Subtype Entailment for Simple Types.
Witold Charatonik & Andreas Podelski
(Max-Planck-Institut für Informatik):
Set Constraints with Intersection.
19:30 Banquet (The Royal Castle)
WEDNESDAY 2 JULY
08:30-10:00 Tutorial
(Chair: Claude Kirchner)
Hubert Comon (LRI, CNRS & Université de Paris-Sud):
Applications of Tree Automata in Rewriting and
Lambda Calculus.
10:00-10:30 Coffee break
10:30-12:00 Semantics & Domain Theory II
(Chair: Pierre-Louis Curien)
Martín Hötzel Escardó (Imperial College, London) &
Thomas Streicher (Technische Hochschule Darmstadt):
Induction and Recursion on the Partial Real Line via
Biquotients of Bifree Algebras.
Martin Hofmann & Thomas Streicher
(Technische Hochschule Darmstadt):
Continuation Models are Universal for
$\lambda\mu$-calculus.
Mariangiola Dezani-Ciancaglini (University of Torino)
Jerzy Tiuryn & Pawel Urzyczyn (University of Warsaw):
Discrimination by Parallel Observers.
12:00-13:30 Lunch
13:30-15:00 Unification and Higher-Order Logic
(Chair: Amy Felty)
Jean Goubault-Larrecq (G.I.E. Dyade)
Ramified Higher-Order Unification.
Iliano Cervesato & Frank Pfenning
(Carnegie Mellon University):
Linear Higher-Order Pre-Unification.
Raymond McDowell & Dale Miller
(University of Pennsylvania):
A Logic for Reasoning with Higher-Order Abstract Syntax.
Leonid Libkin