SATURDAY 20 JUNE
7:30 - 9:30 RECEPTION
SUNDAY 21 JUNE
9:00 - 10:00 Invited talk
Roger Needham (Cambridge University)
Logic and Over-Simplification
(Chair: John Mitchell)
10:00 - 10:30 Coffee break
10:30 - 12:30 Session 1: Finite Model Theory I
(Chair: Martin Otto)
10:30 Fixed-Point Logics on Planar Graphs
Martin Grohe (Institut fur Mathematische Logik,
Freiburg)
10:55 Existential Second-Order Logic over Strings
Thomas Eiter (University of Giessen),
Georg Gottlob (Technische Universitat, Wien),
Yuri Gurevich (University of Michigan)
11:20 - 11:40 Break
11:40 Ordering Finite Variable Types with Generalized Quantifiers
Anuj Dawar (University of Wales), Lauri Hella
(University of Helsinki), Anil Seth (The Institute of
Mathematical Sciences, Madras)
12:05 Convergence Results for Relational Bayesian Networks
Manfred Jaeger (Max-Planck-Institut fur Informatik,
Saarbrucken)
12:30 - 2:00 Lunch
2:00 - 4:35 Session 2: Verification
(Chair: Moshe Y. Vardi)
2:00 The Horn Mu-calculus
Witold Charatonik (Max-Planck-Institut fur Informatik,
Saarbruecken), David McAllester (AT&T Labs), Damian
Niwinski (University of Warsaw), Andreas Podelski
(Max-Planck-Institut fur Informatik, Saarbruecken),
Igor Walukiewicz (University of Warsaw)
2:25 On Model Checking for Non-Deterministic Infinite State
Systems
E. Allen Emerson, Kedar S. Namjoshi (University of
Texas at Austin )
2:50 Freedom, Weakness, and Determinism: From Linear-time to
Branching-time
Orna Kupferman (UC Berkeley), Moshe Y. Vardi (Rice
University)
3:15 - 3:45 Coffee break
3:45 Efficient Representation and Validation of Proofs
George C. Necula, Peter Lee (CMU)
4:10 Secure Implementation of Channel Abstractions
Martin Abadi (DEC), Cedric Fournet,
Georges Gonthier (INRIA)
4:35 - 4:55 Break
4:55 - 5:45 Session 3: Logics
(Chair: Maarten de Rijke)
4:55 The Logical Role of the Four-Valued Bilattice
Ofer Arieli, Arnon Avron (Tel-Aviv University)
5:20 Completeness of a Relational Calculus for Program Schemes
Marcelo F. Frias (Catholic University of Rio de
Janeiro), Roger D. Maddux (Iowa State University)
8:00 Business Meeting
MONDAY 22 JUNE
8:30 - 10:00 Tutorial
Wolfgang Thomas (University of Kiel)
Monadic logic and automata: Recent developments
(Chair: Andre Scedrov)
10:00 - 10:30 Coffee break
10:30 - 12:30 Session 4: Concurrency I
(Chair: Martin Abadi)
10:30 Phase Semantics and Verification of Concurrent
Constraint Programs
Francois Fages (ENS), Paul Ruet (McGill University),
Sylvain Soliman (ENS)
10:55 A Congruence Theorem for Structured Operational
Semantics of Higher-Order Languages
Karen L. Bernstein (DePaul University)
11:20 - 11:40 Break
11:40 Bisimulation in name-passing calculi without matching
Michele Boreale (Universita "La Sapienza"), Davide
Sangiorgi (INRIA)
12:05 The Fusion Calculus: Expressiveness and Symmetry in
Mobile Processes
Joachim Parrow (Royal Institute of Technology, Sweden),
Bjorn Victor (Uppsala University)
12:30 - 2:00 Lunch
2:00 - 4:10 Session 5: Category Theory
(Chair: Eugenio Moggi)
2:00 Type Theory via Exact Categories
L. Birkedal (CMU), A. Carboni (University of Milan),
G. Rosolini (University of Genoa), D.S. Scott (CMU)
2:25 Higher Dimensional Multigraphs
Claudio Hermida, Michael Makkai (McGill University)
John Power (University of Edinburgh)
2:50 - 3:20 Coffee break
3:20 An Axiomatics for Categories of Transition Systems as
Coalgebras
Peter Johnstone (University of Cambridge), John Power
(University of Edinburgh), Toru Tsujishita and Hiroshi
Watanabe (Hokkaido University), James Worrell (Oxford
University)
3:45 A Theory of Recursive Domains with Applications to
Concurrency
Gian Luca Cattani (University of Aarhus), Marcelo
Fiore (University of Sussex), Glynn Winskel
(University of Aarhus)
4:10 - 4:30 Break
4:30 - 6:00 Invited talk
Dirk van Dalen (University of Utrecht)
L.E.J. Brouwer's intuitionism: a revolution in two
installments
(Chair: Bill Rounds)
TUESDAY 23 JUNE
8:30 - 10:00 Tutorial
Maarten de Rijke (University of Amsterdam)
Process Operations in Extended Dynamic Logics
(Chair: Edith Hemaspaandra)
10:00 - 10:30 Coffee break
10:30 - 12:30 Session 6: Theorem Proving and Rewriting
(Chair: Giuseppe Longo)
10:30 Herbrand's theorem, automated reasoning and semantics
tableaux
Andrei Voronkov (Uppsala University)
10:55 The Relation Between Second-Order Unification and
Simultaneous Rigid E-Unification
Margus Veanes (Max-Planck-Institut fur Informatik)
11:20 - 11:40 Break
11:40 Decision Problems in Ordered Rewriting
Hubert Comon (CNRS and LSV), Paliath Narendran (SUNY at
Albany), Robert Nieuwenhuis (Technical University of
Catalonia), Michael Rusinowitch (INRIA and CRIN)
12:05 A Stability Theorem in Rewriting Theory
Paul-Andre Mellies (University of Edinburgh)
12:30 - 2:00 Lunch
2:00 - 3:15 Session 7: Linear Logic
(Chair: Laurent Regnier)
2:00 Light Affine Logic
Andrea Asperti (University of Bologna)
2:25 Linear Logic With Boxes
Ian Mackie (Ecole Polytechnique)
2:50 Coinductive Techniques for Operational Equivalence of
Interaction Nets
Maribel Fernandez (ENS), Ian Mackie (Ecole Polytechnique)
3:15 - 3:45 Coffee break
3:45 - 4:35 Session 8: Game Semantics
(Chair: Dale Miller)
3:45 A fully abstract game semantics for general references
Samson Abramsky, Kohei Honda (University of Edinburgh),
Guy McCusker (St. John's College, Oxford)
4:10 Recursive Types in Games: Axiomatics and Process
Representation
Marcelo Fiore (University of Sussex), Kohei Honda
(University of Edinburgh)
4:35 - 4:55 Break
4:55 - 6:10 Session 9: Type Theory
(Chair: Luke Ong)
4:55 Realizability for Constructive Theory of Functions and
Classes and its Application to Program Synthesis
Makoto Tatsuta (Kyoto University)
5:20 Completeness of Type Assignment Systems with
Intersection, Union, and Type Quantifiers
Hirofumi Yokouchi (Gunma University)
5:45 Full Abstraction for First-Order Objects with Recursive
Types and Subtyping
Ramesh Viswanathan (Bell Laboratories)
7:15 BANQUET (at the Conference Center)
WEDNESDAY 24 JUNE
9:00 - 10:00 Invited talk
Moshe Y. Vardi (Rice University)
Linear time vs. branching time: a complexity-theoretic
perspective
(Chair: Robert Constable)
10:00 - 10:30 Coffee break
10:30 - 11:20 Session 10: Calculus and Lambda-Calculus
(Chair: Vaughan Pratt)
10:30 Calculus in coinductive form
D. Pavlovic (Kestrel Institute), M.H. Escardo
(University of Edinburgh)
10:55 Invertibility in Lambda-Eta
Enno Folkerts (SAP-AG)
11:20 - 11:40 Break
11:40 - 12:30 Session 11: Constraints and Complexity
(Chair: Bengt Jonsson)
11:40 The First-Order Theory of Ordering Constraints over
Feature Trees
Martin Mueller, Joachim Niehren (University of
Saarlandes), Ralf Treinen (University of Paris-South)
12:05 On Proofs About Threshold Circuits and Counting Hierarchies
Jan Johannsen (UCSD), Chris Pollett (Boston University)
12:30 - 2:00 Lunch
2:00 - 3:15 Session 12: Concurrency II
(Chair: Tom Henzinger)
2:00 How to Specify and Verify the Long-Run Average Behavior
of Probabilistic Systems
Luca de Alfaro (UC Berkeley)
2:25 Compositional Analysis of Expected Delays in Networks of
Probabilistic I/O Automata
Eugene W. Stark, Scott A. Smolka (SUNY at Stony Brook)
2:50 A Logical Characterization of Bisimulation for Labeled
Markov Processes
Josee Desharnais (McGill University), Abbas Edalat
(Imperial College), Prakash Panangaden (McGill University)
3:15 - 3:45 Coffee break
3:45 - 5:45 Session 13: Finite Model Theory II
(Chair: Erich Graedel)
3:45 Embedded Finite Models, Stability Theory and the Impact
of Order
John T. Baldwin (University of Illinois at Chicago),
Michael Benedikt (Bell Laboratories)
4:10 On Counting Logics and Local Properties
Leonid Libkin (Bell Laboratories)
4:35 - 4:55 Break
4:55 On the Boundedness Problem for Two-Variable First-Order
Logic
Phokion G. Kolaitis (UC Santa Cruz), Martin Otto (RWTH
Aachen)
5:20 Fragments of existential second-order logic without 0-1
laws
Jean-Marie Le Bars (University of Caen)
[KLEENE PRIZE]