CSDL - Proceedings L

PDF

Reviewers (PDF)

pp. x

PDF

Invited Talk:

Some Decision Problems of Enormous Complexity (Abstract)

Harvey M. Friedman, Ohio State University

pp. 2

PDF

Session 1: Chair: M. Otto

Two-Variable Descriptions of Regularity (Abstract)

Erich Grädel, RWTH Aachen

Eric Rosen, RWTH Aachen

pp. 14

PDF

The Two-Variable Guarded Fragment with Transitive Relations (Abstract)

H. Ganzinger, Max-Planck-Institut f?r Informatik

C. Meyer, Max-Planck-Institut f?r Informatik

M. Veanes, Max-Planck-Institut f?r Informatik

pp. 24

PDF

Logics with Aggregate Operators (Abstract)

Lauri Hella, University of Helsinki

Leonid Libkin, Bell Laboratories

Juha Nurmonen, University of Leicester

Limsoon Wong, Kent Ridge Digital Labs

pp. 35

PDF

Guarded Fixed Point Logic (Abstract)

Erich Grädel, RWTH Aachen

Igor Walukiewicz, Warsaw University

pp. 45

PDF

Session 2: Chair: D. SanGiorgi

Towards a Theory of Bisimulation for Local Names (Abstract)

Alan Jeffrey, DePaul University

Julian Rathke, University of Sussex

pp. 56

PDF

Weak Bisimulation and Open Maps (Abstract)

Marcelo Fiore, University of Sussex

Gian Luca Cattani, University of Cambridge

Glynn Winskel, University of Aarhus

pp. 67

PDF

Elementary Axioms for Categories of Classes (Abstract)

Alex K. Simpson, University of Edinburgh

pp. 77

PDF

Session 3: Chair: M. Dezani

Region Analysis and the Polymorphic Lambda Calculus (Abstract)

Anindya Banerjee, Stevens Institute of Technology

Nevin Heintze, Bell Laboratories, Lucent Technologies

Jon G. Riecke, Bell Laboratories, Lucent Technologies

pp. 88

PDF

Pattern Matching as Cut Elimination (Abstract)

Serenella Cerrito, Universite de Paris-Sud

Delia Kesner, Universite de Paris-Sud

pp. 98

PDF

Some Computational Properties of Intersection Types (Abstract)

Antonio Bucciarelli, Universit? di Roma "La Sapienza"

Silvia de Lorenzis, Universit? di Roma "La Sapienza"

Adolfo Piperno, Universit? di Roma "La Sapienza"

Ivano Salvo, Universit? di Roma "La Sapienza"

pp. 109

PDF

Type Inference for Recursive Definitions (Abstract)

Assaf J. Kfoury, Boston University

Santiago M. Pericas-Geertsen, Boston University

pp. 119

PDF

Plausibility Measures and Default Reasoning: An Overview (Abstract)

Nir Friedman, Hebrew University

Joseph Y. Halpern, Cornell University

pp. 130

PDF

Session 4: Chair: M. Abadi

Subtyping Recursive Types in Kernel Fun - Abstract (Abstract)

Dario Colazzo, University of Pisa

Giorgio Ghelli, University of Pisa

pp. 137

PDF

A Fragment Calculus ? Towards a Model of Separate Compilation, Linking and Binary Compatibility (Abstract)

Sophia Drossopoulou, Imperial College

Susan Eisenbach, Imperial College

David Wragg, Imperial College

pp. 147

PDF

Proof Techniques for Cryptographic Processes (Abstract)

Michele Boreale, Universit? di Roma "La Sapienza"

Rocco de Nicola, Universit? di Firenze

Rosario Pugliese, Universit? di Firenze

pp. 157

PDF

On Hoare Logic and Kleene Algebra with Tests (Abstract)

Dexter Kozen, Cornell University

pp. 167

PDF

Session 5: Chair: G. Dowek

Full Abstraction and Universality via Realisability (Abstract)

Michael Marz, Technische Universit?t Darmstadt

Alexander Rohr, Technische Universit?t Darmstadt

Thomas Streicher, Technische Universit?t Darmstadt

pp. 174

PDF

On Bunched Predicate Logic (Abstract)

David J. Pym, University of London

pp. 183

PDF

Abstract Syntax and Variable Binding (Abstract)

Marcelo Fiore, University of Sussex

Gordon Plotkin, University of Edinburgh

Daniele Turi, University of Edinburgh

pp. 193

PDF

Session 6: Chair: M. Okada

Semantical Analysis of Higher-Order Abstract Syntax (Abstract)

Martin Hofmann

pp. 204

PDF

A New Approach to Abstract Syntax Involving Binders (Abstract)

Murdoch Gabbay, Cambridge University

Andrew Pitts, Cambridge University

pp. 214

PDF

Paramodulation with Non-Monotonic Orderings (Abstract)

Miquel Bofill, Technical University of Catalonia

Guillem Godoy, Technical University of Catalonia

Robert Nieuwenhuis, Technical University of Catalonia

Albert Rubio, Technical University of Catalonia

pp. 225

PDF

Full Completeness of the Multiplicative Linear Logic of Chu Spaces (Abstract)

Harish Devarajan, Stanford University

Dominic Hughes, Stanford University

Vaughan Pratt, Stanford University

Gordon Plotkin, University of Edinburgh

pp. 234

PDF

Cartesian Closed Double Categories, Their Lambda-Notation, and the Pi-Calculus (Abstract)

Roberto Bruni, University of Pisa

Ugo Montanari, University of Pisa

pp. 246

PDF

Session 7: Chair: M. Grohe

Weak Bounded Arithmetic, the Diffie-Hellman Problem and Constable's Class K (Abstract)

Jan Johannsen, University of California at San Diego

pp. 268

PDF

First-Order Logic vs. Fixed-Point Logic in Finite Set Theory (Abstract)

Albert Atserias, University of California at Santa Cruz

Phokion G. Kolaitis, University of California at Santa Cruz

pp. 275

PDF

Entailment of Atomic Set Constraints is PSPACE-Complete (Abstract)

Joachim Niehren, Universit?t des Saarlandes

Martin Müller, Universit?t des Saarlandes

Jean-Marc Talbot, Max-Planck Institut Informatik

pp. 285

PDF

A Superposition Decision Procedure for the Guarded Fragment with Equality (Abstract)

H. Ganzinger

H. de Nivelle

pp. 295

PDF

Session 8: Chair: S. Weinstein

Working with Arms: Complexity Results on Atomic Representations of Herbrand Models (Abstract)

Georg Gottlob, Technische Universit?t Wien

Reinhard Pichler, Technische Universit?t Wien

pp. 306

PDF

Logics with Counting, Auxiliary Relations, and Lower Bounds for Invariant Queries (Abstract)

Leonid Libkin, Bell Laboratories/INRIA

pp. 316

PDF

Counting and Addition cannot Express Deterministic Transitive Closure (Abstract)

Matthias Ruhl, Massachusetts Institute of Technology

pp. 326

PDF

Session 9: Chair: N. Shankar

Parametric Quantitative Temporal Reasoning (Abstract)

E. Allen Emerson, University of Texas at Austin

Richard J. Trefler, University of Texas at Austin

pp. 336

PDF

Modular Temporal Logic (Abstract)

Augustin Baziramwabo, Universite de Montreal

Pierre McKenzie, Universite de Montreal

Denis Thérien, McGill University

pp. 344

PDF

On the Verification of Broadcast Protocols (Abstract)

Javier Esparza, Technische Universit?t M?nchen

Alain Finkel, ENS de Cachan

Richard Mayr, University of Edinburgh

pp. 352

PDF

On the Expressive Power of CTL (Abstract)

Faron Moller, Uppsala University

Alexander Rabinovich, Tel Aviv University

pp. 360

PDF

Proving Security Protocols Correct (Abstract)

Lawrence C. Paulson

pp. 370

PDF

Session 10: Chair: E. Robinson

Reasoning About Common Knowledge with Infinitely Many Agents (Abstract)

Joseph Y. Halpern, Cornell University

Richard A. Shore, Cornell University

pp. 384

PDF

Parikh's Theorem in Commutative Kleene Algebra (Abstract)

Mark W. Hopkins, Adaptive Micro Systems, Inc.

Dexter C. Kozen, Cornell University

pp. 394

PDF

The Higher-Order Recursive Path Ordering (Abstract)

J.-P. Jouannaud, Universit? de Paris Sud

A. Rubio, University Polit?cnica de Catalunya

pp. 402

PDF

Extensional Equality in Intensional Type Theory (Abstract)

Thorsten Altenkirch, University of Munich

pp. 412

PDF

Session 11: Chair: V. Danos

A Fully Abstract Game Semantics for Finite Nondeterminism (Abstract)

Russell Harmer, Imperial College, London

Guy McCusker, University of Sussex

pp. 422

PDF

Concurrent Games and Full Completeness (Abstract)

Samson Abramsky, University of Edinburgh

Paul-André Melliès, University Paris 7

pp. 431

PDF

Non-Deterministic Games and Program Analysis: An Application to Security (Abstract)

Pasquale Malacaria, Imperial College

Chris Hankin, Imperial College

pp. 443

PDF

Session 12: Chair: A. Asperti

Correctness of Multiplicative Proof Nets is Linear (Abstract)

Stefano Guerrini, Universit? di Roma I, "La Sapienza"

pp. 454

PDF

Linear Types and Non Size-Increasing Polynomial Time Computation (Abstract)

Martin Hofmann

pp. 464

PDF

Author Index (PDF)

pp. 477