The Community for Technology Leaders
Logic in Computer Science, Symposium on (2003)
Ottawa, Canada
June 22, 2003 to June 25, 2003
ISSN: 1043-6871
ISBN: 0-7695-1884-2

Foreword (PDF)

pp. x
Session 1

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
Session 2
Session 3

Reasoning about Hierarchical Storage (Abstract)

Amal Ahmed , Princeton University
Limin Jia , Princeton University
David Walker , Princeton University
pp. 33

Formal Verification at Intel (Abstract)

John Harrison , Intel Corporation
pp. 45
Session 4

Abstract Saturation-Based Inference (Abstract)

Nachum Dershowitz , Tel-Aviv University
Claude Kirchner , LORIA & INRIA
pp. 65

Orienting Equalities with the Knuth-Bendix Order (Abstract)

Konstantin Korovin , MPI Informatik
Andrei Voronkov , University of Manchester
pp. 75
Short Presentations I
Session 5

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

Viktor Kuncak , Massachusetts Institute of Technology
Martin Rinard , Massachusetts Institute of Technology
pp. 96

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

Andrzej S. Murawski , Oxford University Computing Laboratory
pp. 108
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

Polynomial-time Algorithms from Ineffective Proofs (Abstract)

Paulo Oliva , University of Aarhus, Denmark
pp. 128

The Complexity of Resolution Refinements (Abstract)

Joshua Buresh-Oppenheim , University of Toronto
Toniann Pitassi , University of Toronto
pp. 138
Session 7
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

Logical Definability and Query Languages over Unranked Trees (Abstract)

Leonid Libkin , University of Toronto
Frank Neven , University of Limburg
pp. 178
Session 9

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

Jo? Ouaknine , Carnegie Mellon University
James Worrell , Tulane University
pp. 198
Session 10

Logic in Access Control (Abstract)

Mart? Abadi , University of California at Santa Cruz
pp. 228
Session 11

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

Marco Pistore , University of Trento
Moshe Y. Vardi , Rice University
pp. 234


John McCarthy , Stanford University
pp. 244
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

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
Session 13

Spectrum Hierarchies and Subdiagonal Functions (Abstract)

Aaron Hunter , Simon Fraser University
pp. 281
Session 14

Homomorphism Closed vs. Existential Positive (Abstract)

Tom? Feder , Stanford University
Moshe Y. Vardi , Rice University
pp. 311

Tractable conservative Constraint Satisfaction Problems (Abstract)

Andrei A. Bulatov , Oxford University Computing Laboratory
pp. 321
Session 15

Labelled Markov Processes: Stronger and Faster Approximations (Abstract)

Vincent Danos , CNRS & Université Paris 7
Jos? Desharnais , Universit? Laval
pp. 341
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

Model-checking Trace Event Structures (Abstract)

P. Madhusudan , University of Pennsylvania
pp. 371
Short Presentations II

Author's Index (PDF)

pp. 393
93 ms
(Ver 3.3 (11022016))