CSDL - Proceedings L

Conference Organization (PDF)

pp. xi

Program Committee (PDF)

pp. xii

Additional Reviewers (PDF)

pp. xiii

Session 1

Proof Nets for Unit-free Multiplicative-Additive Linear Logic (Extended abstract) (Abstract)

DOMINIC HUGHES, Stanford University

ROB VAN GLABBEEK, Stanford University

pp. 1

PDF

About Translations of Classical Logic into Polarized Linear Logic (Abstract)

Olivier Laurent, Preuves Programmes Syst?mes

Laurent Regnier, Institut de Math?matiques de Luminy

pp. 11

PDF

System ST \beta-reduction and completeness (Abstract)

Christophe Raffalli, Universit? de Savoie

pp. 21

PDF

Session 2

Types and Programming Languages: The Next Generation (PDF)

Benjamin C. Pierce, University of Pennsylvania

pp. 32

Session 3

Reasoning about Hierarchical Storage (Abstract)

Amal Ahmed, Princeton University

Limin Jia, Princeton University

David Walker, Princeton University

pp. 33

PDF

Formal Verification at Intel (Abstract)

John Harrison, Intel Corporation

pp. 45

PDF

Session 4

New Directions in Instantiation-Based Theorem Proving (Abstract)

Harald Ganzinger, MPI Informatik

Konstantin Korovin, MPI Informatik

pp. 55

PDF

Abstract Saturation-Based Inference (Abstract)

Nachum Dershowitz, Tel-Aviv University

Claude Kirchner, LORIA & INRIA

pp. 65

PDF

Orienting Equalities with the Knuth-Bendix Order (Abstract)

Konstantin Korovin, MPI Informatik

Andrei Voronkov, University of Manchester

pp. 75

PDF

Short Presentations I

Practical Reflection in Nuprl

An Applicative-Order Term Rewriting System for Code Generation, and Its Termination Analysis

Patterns Based on Multiple Interacting Partial Orders

Logic of Subtyping

A Language and a Notion of Truth for Cryptographic Properties

The Relative Complexity of Local Search Heuristics and the Iteration Principle

A Second-Order Theory for NL

Session 5

Dependent Intersection: A New Way of Defining Records in Type Theory (Abstract)

Alexei Kopylov, Cornell University

pp. 86

PDF

Structural Subtyping of Non-Recursive Types is Decidable (Abstract)

Viktor Kuncak, Massachusetts Institute of Technology

Martin Rinard, Massachusetts Institute of Technology

pp. 96

PDF

On Program Equivalence in Languages with Ground-Type References (Abstract)

Andrzej S. Murawski, Oxford University Computing Laboratory

pp. 108

PDF

Session 6

A Proof Theory for Generic Judgments: An extended abstract (Abstract)

Dale Miller, INRIA/Futurs/Saclay & ?cole polytechnique

Alwen Tiu, ?cole polytechnique & Penn State University

pp. 118

PDF

Polynomial-time Algorithms from Ineffective Proofs (Abstract)

Paulo Oliva, University of Aarhus, Denmark

pp. 128

PDF

The Complexity of Resolution Refinements (Abstract)

Joshua Buresh-Oppenheim, University of Toronto

Toniann Pitassi, University of Toronto

pp. 138

PDF

Session 7

Successor-Invariance in the Finite (Abstract)

Benjamin Rossman

pp. 148

PDF

Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions (Abstract)

Erich Gr?del, Aachen University

Stephan Kreutzer, University of Edinburgh

pp. 158

PDF

Session 8

On Automatic Partial Orders (Abstract)

Bakhadyr Khoussainov, University of Auckland, New Zealand

Sasha Rubin, University of Auckland, New Zealand

Frank Stephan, University of Heidelberg, Germany

pp. 168

PDF

Logical Definability and Query Languages over Unranked Trees (Abstract)

Leonid Libkin, University of Toronto

Frank Neven, University of Limburg

pp. 178

PDF

Query Evaluation on Compressed Trees (Extended Abstract) (Abstract)

pp. 188

PDF

Session 9

Revisiting Digitization, Robustness, and Decidability for Timed Automata (Abstract)

Jo? Ouaknine, Carnegie Mellon University

James Worrell, Tulane University

pp. 198

PDF

Satisfiability in Alternating-time Temporal Logic (Abstract)

Govert van Drimmelen, Rand Afrikaans University

pp. 208

PDF

Petr Jancar, Techn. Univ. Ostrava

pp. 218

PDF

Session 10

Logic in Access Control (Abstract)

Mart? Abadi, University of California at Santa Cruz

pp. 228

PDF

Session 11

The Planning Spectrum - One, Two, Three, Infinity (Abstract)

Marco Pistore, University of Trento

Moshe Y. Vardi, Rice University

pp. 234

PDF

ADVICE ABOUT LOGICAL AI (Abstract)

John McCarthy, Stanford University

pp. 244

PDF

Session 12

A Sound Framework for Untrusted Verification-Condition Generators (Abstract)

George C. Necula, University of California, Berkeley

Robert R. Schneck, University of California, Berkeley

pp. 248

PDF

An NP Decision Procedure for Protocol Insecurity with XOR (Abstract)

Yannick Chevalier, Universit? Henri Poincar?

Ralf K?sters, Stanford University

Micha? Rusinowitch, Universit? Henri Poincar?

Mathieu Turuani, Universit? Henri Poincar?

pp. 261

PDF

Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or (Abstract)

H. Comon-Lundh, LSV, INRIA and ENS Cachan

V. Shmatikov, SRI International

pp. 271

PDF

Session 13

Spectrum Hierarchies and Subdiagonal Functions (Abstract)

Aaron Hunter, Simon Fraser University

pp. 281

PDF

Spectra of Monadic Second-Order Formulas with One Unary Function (Abstract)

Yuri Gurevich, Microsoft Research

Saharon Shelah, Hebrew University

pp. 291

PDF

Convergence Law for Random Graphs with Specified Degree Sequence (Abstract)

James F. Lynch, Clarkson University

pp. 301

PDF

Session 14

Homomorphism Closed vs. Existential Positive (Abstract)

Tom? Feder, Stanford University

Moshe Y. Vardi, Rice University

pp. 311

PDF

Tractable conservative Constraint Satisfaction Problems (Abstract)

Andrei A. Bulatov, Oxford University Computing Laboratory

pp. 321

PDF

A Constraint-Based Presentation and Generalization of Rows (Abstract)

Fran?ois Pottier, INRIA

pp. 331

PDF

Session 15

Labelled Markov Processes: Stronger and Faster Approximations (Abstract)

Vincent Danos, CNRS & Université Paris 7

Jos? Desharnais, Universit? Laval

pp. 341

PDF

Model checking for probability and time: from theory to practice (Abstract)

Marta Kwiatkowska, University of Birmingham

pp. 351

PDF

Session 16

Model Checking Guarded Protocols (Abstract)

E. Allen Emerson, The University of Texas at Austin

Vineet Kahlon, The University of Texas at Austin

pp. 361

PDF

Model-checking Trace Event Structures (Abstract)

P. Madhusudan, University of Pennsylvania

pp. 371

PDF

Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems (Abstract)

Nir Piterman, The Weizmann Institute of Science

Moshe Y. Vardi, Rice University

pp. 381

PDF

Short Presentations II

A Proposal to Extend Abstract State Machines to Applications in Systems Biology

Stuttering Refinement on Partial Systems

Assume-Guarantee Reasoning with Features

Modularity Theorems for Non-Monotone Induction

Linear-Time Algorithms for Monadic Logic

Game-Based Notions of Locality

Arb:An Implementation of Selecting Tree Automata for XML Query Processing

Author's Index (PDF)

pp. 393