18. LICS 2003: Ottawa, Canada

18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings. IEEE Computer Society 2003, ISBN 0-7695-1884-2

Session 1

Dominic J. D. Hughes, Rob J. van Glabbeek:
Proof Nets for Unit-free Multiplicative-Additive Linear Logic (Extended abstract). 1-10
Olivier Laurent, Laurent Regnier:
About Translations of Classical Logic into Polarized Linear Logic. 11-20
Christophe Raffalli:
System ST \beta-reduction and completeness. 21-

Session 2

Benjamin C. Pierce:
Types and Programming Languages: The Next Generation. 32-

Session 3

Amal J. Ahmed, Limin Jia, David Walker:
Reasoning about Hierarchical Storage. 33-44
John Harrison:
Formal Verification at Intel. 45-

Session 4

Harald Ganzinger, Konstantin Korovin:
New Directions in Instantiation-Based Theorem Proving. 55-64
Nachum Dershowitz, Claude Kirchner:
Abstract Saturation-Based Inference. 65-74
Konstantin Korovin, Andrei Voronkov:
Orienting Equalities with the Knuth-Bendix Order. 75-

Session 5

Alexei Kopylov:
Dependent Intersection: A New Way of Defining Records in Type Theory. 86-95
Viktor Kuncak, Martin C. Rinard:
Structural Subtyping of Non-Recursive Types is Decidable. 96-107
Andrzej S. Murawski:
On Program Equivalence in Languages with Ground-Type References. 108-

Session 6

Dale Miller, Alwen Fernanto Tiu:
A Proof Theory for Generic Judgments: An extended abstract. 118-127
Paulo Oliva:
Polynomial-time Algorithms from Ineffective Proofs. 128-137
Josh Buresh-Oppenheim, Toniann Pitassi:
The Complexity of Resolution Refinements. 138-

Session 7

Benjamin Rossman:
Successor-Invariance in the Finite. 148-
Erich Grädel, Stephan Kreutzer:
Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions. 158-

Session 8

Bakhadyr Khoussainov, Sasha Rubin, Frank Stephan:
On Automatic Partial Orders. 168-177
Leonid Libkin, Frank Neven:
Logical Definability and Query Languages over Unranked Trees. 178-187
Markus Frick, Martin Grohe, Christoph Koch:
Query Evaluation on Compressed Trees (Extended Abstract). 188-

Session 9

Joël Ouaknine, James Worrell:
Revisiting Digitization, Robustness, and Decidability for Timed Automata. 198-207
Govert van Drimmelen:
Satisfiability in Alternating-time Temporal Logic. 208-217
Petr Jancar:
Strong Bisimilarity on Basic Parallel Processes is PSPACE-complete. 218-

Session 10

Martín Abadi:
Logic in Access Control. 228-

Session 11

Marco Pistore, Moshe Y. Vardi:
The Planning Spectrum - One, Two, Three, Infinity. 234-243
John McCarthy:
Advice about logical AI. 244-

Session 12

George C. Necula, Robert R. Schneck:
A Sound Framework for Untrusted Verification-Condition Generators. 248-260
Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, Mathieu Turuani:
An NP Decision Procedure for Protocol Insecurity with XOR. 261-270
Hubert Comon-Lundh, Vitaly Shmatikov:
Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or. 271-

Session 13

Aaron Hunter:
Spectrum Hierarchies and Subdiagonal Functions. 281-290
Yuri Gurevich, Saharon Shelah:
Spectra of Monadic Second-Order Formulas with One Unary Function. 291-300
James F. Lynch:
Convergence Law for Random Graphs with Specified Degree Sequence. 301-

Session 14

Tomás Feder, Moshe Y. Vardi:
Homomorphism Closed vs. Existential Positive. 311-320
Andrei A. Bulatov:
Tractable conservative Constraint Satisfaction Problems. 321-

Session 15

Vincent Danos, Josee Desharnais:
Labelled Markov Processes: Stronger and Faster Approximations. 341-350
Marta Z. Kwiatkowska:
Model checking for probability and time: from theory to practice . 351-

Session 16

E. Allen Emerson, Vineet Kahlon:
Model Checking Guarded Protocols. 361-370
P. Madhusudan:
Model-checking Trace Event Structures. 371-380
Nir Piterman, Moshe Y. Vardi:
Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems. 381-

Last update Mon Feb 13 04:36:42 2012 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page