CSDL - Proceedings L

Conference Organization (PDF)

pp. xi

Additional Reviewers (PDF)

pp. xii

Invited Talk - Chair: Joseph Y. Halpern

Probabilistic Polynomial-Time Process Calculus and Security Protocol Analysis (Abstract)

J. Mitchell, Stanford University

A. Ramanathan, Stanford University

V. Teague, Stanford University

A. Scedrov, University of Pennsylvania

pp. 0003

PDF

Session 1 - Chair: Jean-Pierre Jouannaud

Definitions by Rewriting in the Calculus of Constructions (Abstract)

Frédéric Blanqui, Universit? Paris-Sud

pp. 0009

PDF

Deconstructing Shostak (Abstract)

Harald Rueß, SRI International

Natarajan Shankar, SRI International

pp. 0019

PDF

A Decision Procedure for an Extensional Theory of Arrays (Abstract)

Aaron Stump, Stanford University

Clark W. Barrett, Stanford University

David L. Dill, Stanford University

Jeremy Levitt, 0-In Design Automation, Inc.

pp. 0029

PDF

On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups (Abstract)

Guillem Godoy, Technical University of Catalonia

Robert Nieuwenhuis, Technical University of Catalonia

pp. 0038

PDF

Invited Talk - Chair: Jean-Pierre Jouannaud

Successive Approximation of Abstract Transition Relations (Abstract)

Satyaki Das, Stanford University

David L. Dill, Stanford University

pp. 0051

PDF

Session 2 - Chair: Pawel Urzyczyn

A Bound on Attacks on Payment Protocols (Abstract)

Scott D. Stoller, SUNY at Stony Brook

pp. 0061

PDF

Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems (Abstract)

Harald Ganzinger, Max-Planck-Institut fur Informatik

pp. 0081

PDF

Session 3 - Chair: Radha Jaghadeesan

Semantics of Name and Value Passing (Abstract)

Marcelo Fiore, University of Cambridge

Daniele Turi, University of Edinburgh

pp. 0093

PDF

A Fully Abstract Game Semantics of Local Exceptions (Abstract)

J. Laird, University of Sussex

pp. 0105

PDF

A Universal Characterization of the Closed Euclidean Interval (Abstract)

Martín H. Escardó, University of Birmingham

Alex K. Simpson, University of Edinburgh

pp. 0115

PDF

Invited Talk - Chair: Gordon Plotkin

Logician in the Land of OS: Abstract State Machines in Microsoft (Abstract)

Yuri Gurevich, Microsoft Research

pp. 0129

PDF

Session 4 - Chair: Michel de Rougemont

Eliminating Definitions and Skolem Functions in First-Order Logic (Abstract)

Jeremy Avigad, Carnegie Mellon University

pp. 0139

PDF

On the Decision Problem for the Guarded Fragment with Transitivity (Abstract)

Wieslaw Szwast, Opole University

Lidia Tendera, Opole University

pp. 0147

PDF

The Hierarchy inside Closed Monadic S1 Collapses on the Infinite Binary Tree (Abstract)

Giacomo Lenzi. Andre Arnold, Universit? de Bordeaux

Jerzy Marcinkowski, University of Wroclaw

pp. 0157

PDF

On Definability of Order in Logic with Choice (Abstract)

Taneli Huuskonen, University of Helsinki

Tapani Hyttinen, University of Helsinki

pp. 0167

PDF

Invited Talk - Chair: Erich Graedel

The Engineering Challenge for Logic

Session 5 - Chair: Erich Graedel

A Second-Order System for Polytime Reasoning Using Gr?del's Theorem (Abstract)

Stephen Cook, University of Toronto

Antonina Kolokolova, University of Toronto

pp. 0177

PDF

The Crane Beach Conjecture (Abstract)

David A. Mix Barrington, University of Massachusetts

Neil Immerman, University of Massachusetts

Clemens Lautemann, Johannes Gutenberg-Universit?t Mainz

Nicole Schweikardt, Johannes Gutenberg-Universit?t Mainz

Denis Thérien, McGill University

pp. 0187

PDF

An n! Lower Bound on Formula Size (Abstract)

Micah Adler, UMass, Amherst

Neil Immerman, UMass, Amherst

pp. 0197

PDF

Session 6 - Chair: Nevin Heintze

Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory (Abstract)

Frank Pfenning, Carnegie Mellon University

pp. 0221

PDF

Dependent Types for Program Termination Verification (Abstract)

Hongwei Xi, University of Cincinnati

pp. 0231

PDF

Short Paper Session - Chair: Joseph Y. Halpern

The Dolev-Yaho Intruder is the Most Powerful Attacker

Semantics of machine Instructions at Multiple Levels of Abstraction

A proof-Carrying Authorization System

Recursive Programming Languages for Complexity Classes

Interior-Point Approach to Parity Games

Recent Progress in Proof Mining

On the Complexity of Confluence for Ground Rewrite Systems

Computing the Density of Regular Languages

Integrating Simplification Techniques in SAT Algorithms

Basic Completion Modulo with Simplification

Finite Visit Sequential Deterministic Tree Automata

Invited Talk - Chair: Ron van der Meyden

Foundational Proof-Carrying Code (Abstract)

Andrew W. Appel, Princeton University

pp. 0247

PDF

Session 7 - Chair: Parosh Abdulla

Intuitionistic Linear Logic and Partial Correctness (Abstract)

Dexter Kozen, Cornell University

Jerzy Tiuryn, Warsaw University

pp. 0259

PDF

Perturbed Turing Machines and Hybrid Systems (Abstract)

Eugene Asarin, VERIMAG

Ahmed Bouajjani, LIAFA, University of Paris 7

pp. 0269

PDF

Deterministic Generators and Games for Ltl Fragments (Abstract)

Rajeev Alur, University of Pennsylvania

Salvatore La Torre, University of Pennsylvania

pp. 0291

PDF

Session 8 - Chair: Adolfo Piperno

Normalization by Evaluation for Typed Lambda Calculus with Coproducts (Abstract)

pp. 0303

PDF

A Symbolic Labelled Transition System for Coinductive Subtyping of F_{\mu\leq} Types (Abstract)

Alan Jeffrey, DePaul University

pp. 0323

PDF

A Continuum of Theories of Lambda Calculus without Semantics (Abstract)

Antonino Salibra, Universit? di Venezia

pp. 0334

PDF

Session 9 - Chair: Hubert Comon

Focus Games for Satisfiability and Completeness of Temporal Logic (Abstract)

Martin Lange, University of Edinburgh

Colin Stirling, University of Edinburgh

pp. 0357

PDF

Safety and Liveness in Branching Time (Abstract)

Panagiotis Manolios, University of Texas, Austin

Richard Trefler, AT&T Labs-Research

pp. 0366

PDF

Short Papers

Self-Verifying Systems, the Incompleteness Theorem and the Tangibility Reflection Principle

Repairing the Interpolation Theorem in First-Order Modal Logic

A Game involving Epistemic Logic and Probability

A Theory of Advanced Transactions in the Situation Calculus

Invited Talk - Chair: Michel de Rougemont

Semistructured Data: From Practice to Theory (Abstract)

Serge Abiteboul

pp. 0379

PDF

Session 10 - Chair: Rance Cleaveland

Synthesizing Distributed Systems (Abstract)

Orna Kupferman, Hebrew University

Moshe Y. Vardi, Rice University

pp. 0389

PDF

Permutation Rewriting and Algorithmic Verification (Abstract)

Ahmed Bouajjani, LIAFA, Universit? Paris VII

Anca Muscholl, LIAFA, Universit? Paris VII

Tayssir Touili, LIAFA, Universit? Paris VII

pp. 0399

PDF

Temporal Logic Query Checking (Abstract)

Glenn Bruns, Bell Laboratories, Lucent Technologies

Patrice Godefroid, Bell Laboratories, Lucent Technologies

pp. 0409

PDF

Session 11 - Chair: Ron van der Meyden

Typechecking XML Views of Relational Databases (Abstract)

Noga Alon, Tel Aviv University

Tova Milo, Tel Aviv University

Frank Neven, Limburgs Universitair Centrum

Dan Suciu, University of Washington

Victor Vianu, U.C. San Diego

pp. 0421

PDF

A Model-Theoretic Approach to Regular String Relations (Abstract)

Michael Benedikt, Bell Labs

Leonid Libkin, U. Toronto

Thomas Schwentick, U. Jena

Luc Segoufin, INRIA

pp. 0431

PDF

Author Index (PDF)

pp. 0441