Regular papers

Amal Ahmed, Andrew W. Appel, and Roberto Virga; Princeton U, USA
A stratified semantics of general references embeddable in higher-order logic

Albert Atserias, Techn. U of Catalonia, Spain
Unsatisfiable random formulas are hard to certify

Jean-Marie Le Bars, U Caen, France
The 0-1 law fails for frame satisfiability of propositional modal logic

Michael Benedikt, Bell Labs, USA and Leonid Libkin, U Toronto, Canada
Tree extension algebras: Logics, automata, and query languages

Edmund M. Clarke, Carnegie Mellon U, USA; Somesh Jha, U Wisconsin-Madison, USA; Yuan Lu, Broadcom, USA; and Helmut Veith, Vienna U of Techn., Austria
Tree-like counterexamples in model checking

Josée Desharnais, Laval U, Canada; Vineet Gupta, Stratify Inc., USA; Radha Jagadeesan, Loyola U Chicago, USA; and Prakash Panangaden, McGill U, Canada
The metric analogue of weak bisimulation for probabilistic processes

Catalin Dima, IMAG Grenoble, France
Computing reachability relations in timed automata

Abbas Edalat, Imperial College, UK and Andre Lieutier, Dassault Systemes Provence and LMC/IMAG, France
Domain theory and differential calculus (functions of one variable)

Marco Faella, Salvatore La Torre, and Aniello Murano; U Salerno, Italy
Dense real-time games

Marcelo Fiore, U Cambridge, UK; Roberto Di Cosmo, U Paris VII, France; and Vincent Balat, U Paris VII, France
Remarks on isomorphisms in typed lambda calculi with empty and sum types

Markus Frick and Martin Grohe, U Edinburgh, UK
The complexity of first-order and monadic second-order logic revisited

Alain Frisch, ENS Paris, France; Giuseppe Castagna, ENS Paris, France; and Véronique Benzaken, U Paris XI (Paris-Sud), France
Semantic subtyping

Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and Zhaozhong Ni; Yale U, USA
A syntactic approach to foundational proof-carrying code

William Hesse and Neil Immerman, U Massachusetts, USA
Complete problems for dynamic complexity classes

Daniel Hirschkoff, ENS Lyon, France; Etienne Lozes, ENS Lyon, France; and Davide Sangiorgi, INRIA Sophia-Antipolis, France
Separability, expressiveness, and decidability in the ambient logic

Ian Hodkinson, Imperial College, UK; Frank Wolter, U Leipzig, Germany; and Michael Zakharyaschev, King's College London, UK
Decidable and undecidable fragments of first-order branching temporal logics

Martin Hyland and Andrea Schalk, U Cambridge, UK
Games on graphs and sequantially realizable functionals

Hajime Ishihara, Japan Advanced Inst. of Science and Techn., Japan; Bakhadyr Khoussainov, U Auckland, New Zealand; and Sasha Rubin, U Auckland, New Zealand
Some results on automatic structures

Alan Jeffrey, DePaul U, USA and Julian Rathke, U Sussex, UK
A fully abstract may testing semantics for concurrent objects

Stephan Kreutzer, Aachen U of Techn., Germany
Expressive equivalence of least and inflationary fixed-point logic

Sophie Laplante, U Paris XI (Paris-Sud), France; Richard Lassaigne, U Paris VII, France; Frederic Magniez, U Paris XI (Paris-Sud), France; Sylvain Peyronnet, U Paris XI (Paris-Sud), France; and Michel de Rougemont, U Paris II, France
Probabilistic abstraction for model checking: An approach based on property testing

François Laroussinie, Nicolas Markey, and Philippe Schnoebelen; ENS Cachan, France
Temporal logic with forgettable past

Olivier Laurent, U Paris VII, France
Polarized games

Daniel Leivant, Indiana U Bloomington, USA
Calibrating computational feasibility by abstraction rank

Christopher Lynch and Barbara Morawska, Clarkson U, USA
Automatic decidability

Mikkel Nygaard, U Aarhus, Denmark and Glynn Winskel, U Cambridge, UK
Linearity in process languages

C.-H. L. Ong, Oxford U, UK
Observational equivalence of 3rd-order idealized Algol is decidable

Martin Otto, U Wales Swansea, UK
Modal and guarded characterisation theorems over finite transition systems

Jens Palsberg and Tian Zhao, Purdue U, USA
Efficient type inference for record concatenation and subtyping

Thomas Reps, U Wisconsin-Madison, USA; Alexey Loginov, U Wisconsin-Madison, USA; and Mooly Sagiv, Tel Aviv U, Israel
Semantic minimization of 3-valued propositional formulae

Bernhard Reus, U Sussex, UK and Thomas Streicher, U Darmstadt, Germany
Semantics and logic of object calculi

Alex Simpson, U Edinburgh, UK
Computational adequacy for recursive types in models of intuitionistic set theory

Michael Soltys, McMaster U, Canada and Stephen A. Cook, U Toronto, Canada
The proof complexity of linear algebra

Richard Statman, Carnegie Mellon U, USA
On the lambda Y calculus

Ashish Tiwari, SRI International, USA
Deciding confluence of certain term rewriting systems in polynomial time

Daniele Varacca, U Aarhus, Denmark
The powerdomain of indexed valuations

Short presentations

Emmanuel Beffara, ENS Lyon, France and Sergei Vorobyov, Uppsala U, Sweden
Is randomized Gurvich-Karzanov-Khachiyan's algorithm for parity games polynomial?

Henrik Björklund and Sergei Vorobyov, Uppsala U, Sweden
Two adversary lower bounds for parity games

Emanuele Covino and Giovanni Pani, U Bari, Italy
Time-space computational complexity of imperative programming languages

Claudia Faggian, U Cambridge, UK
Ludics dynamics: Designs and interactive observability

Jonathan Ford, U New England, Australia; Ian A. Mason, U New England, Australia; and Natarajan Shankar, SRI International, USA
Lessons learned from formal developments in PVS

Jens Chr. Godskesen, IT U of Copenhagen, Denmark; Thomas Hildebrandt, IT U of Copenhagen, Denmark; and Vladimiro Sassone, U Sussex, UK
An overview of MR, a calculus of mobile resources

Sylvain Soliman, INRIA Rocquencourt, France
CLP implementation of a phase model checker