Logic in computer science. proceedings : 18th Annual IEEE Symposium on Logic in Computer Science : 22-25 July, 2003, Ottawa, Canada / sponsored by IEEE Computer Society Technical Committee on Mathematical Foundations of Computing in cooperation with Association for Symbolic Logic, European Association for Theoretical Computer Science.

Format:

Book

Conference/Event

Contributor:

IEEE Xplore (Online service)

IEEE Computer Society. Technical Committee on Mathematical Foundations of Computing.

Conference Name:

Symposium on Logic in Computer Science (18th : 2003 : Ottawa, Canada)

Language:

English

Subjects (All):

Computer science--Mathematics--Congresses.

Computer science.

Computer science--Mathematics.

Logic, Symbolic and mathematical--Congresses.

Logic, Symbolic and mathematical.

Genre:

Conference papers and proceedings.

Physical Description:

xiv, 393 pages : illustrations

Other Title:

IEEE Symposium on Logic in Computer Science

Also known as: LICS 2003

Place of Publication:

Los Alamitos, Calif. : IEEE Computer Society, [2003]

System Details:

Mode of access: World Wide Web.

text file

Contents:

Proof Nets for Unit-Free Multiplicative-Additive Linear Logic / D. Hughes, R. van Glabbeek 1

About Translations of Classical Logic into Polarized Linear Logic / O. Laurent, L. Regnier 11

System ST [beta]-Reduction and Completeness / C. Raffalli 21

Invited Tutorial

Types and Programming Languages: The Next Generation / B. C. Pierce 32

Reasoning about Hierarchical Storage / A. Ahmed, L. Jia, D. Walker 33

Invited Talk

Formal Verification at Intel / J. Harrison 45

New Directions in Instantiation-Based Theorem Proving / H. Ganzinger, K. Korovin 55

Abstract Saturation-Based Inference / N. Dershowitz, C. Kirchner 65

Orienting Equalities with the Knuth-Bendix Order / K. Korovin, A. Voronkov 75

Practical Reflection in Nuprl / E. Barzilay, S. Allen, R. Constable

An Applicative-Order Term Rewriting System for Code Generation, and Its Termination Analysis / O. Kiselyov

Patterns Based on Multiple Interacting Partial Orders / F. J. Oles

Logic of Subtyping / P. Naumov

A Language and a Notion of Truth for Cryptographic Properties / S. Kramer

The Relative Complexity of Local Search Heuristics and the Iteration Principle / T. Morioka

A Second-Order Theory for NL / S. Cook, A. Kolokolova

Dependent Intersection: A New Way of Defining Records in Type Theory / A. Kopylov 86

Structural Subtyping of Non-Recursive Types Is Decidable / V. Kuncak, M. Rinard 96

On Program Equivalence in Languages with Ground-Type References / A. S. Murawski 108

A Proof Theory for Generic Judgments: An Extended Abstract / D. Miller, A. Tiu 118

Polynomial-Time Algorithms from Ineffective Proofs / P. Oliva 128

The Complexity of Resolution Refinements / J. Buresh-Oppenheim, T. Pitassi 138

Successor-Invariance in the Finite / B. Rossman 148

Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions / E. Gradel, S. Kreutzer 158

On Automatic Partial Orders / B. Khoussainov, S. Rubin, F. Stephan 168

Logical Definability and Query Languages over Unranked Trees / L. Libkin, F. Neven 178

Query Evaluation on Compressed Trees / M. Frick, M. Grohe, C. Koch 188

Revisiting Digitization, Robustness, and Decidability for Timed Automata / J. Ouaknine, J. Worrell 198

Satisfiability in Alternating-Time Temporal Logic / G. van Drimmelen 208

Strong Bisimilarity on Basic Parallel Processes Is PSPACE-Complete / P. Jancar 218

Logic in Access Control / M. Abadi 228

The Planning Spectrum

One, Two, Three, Infinity / M. Pistore, M. Y. Vardi 234

Advice about Logical AI / J. McCarthy 244

A Sound Framework for Untrusted Verification-Condition Generators / G. C. Necula, R. R. Schneck 248

An NP Decision Procedure for Protocol Insecurity with XOR / Y. Chevalier, R. Kusters, M. Rusinowitch, M. Turuani 261

Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or / H. Comon-Lundh, V. Shmatikov 271

Spectrum Hierarchies and Subdiagonal Functions / A. Hunter 281

Spectra of Monadic Second-Order Formulas with One Unary Function / Y. Gurevich, S. Shelah 291

Convergence Law for Random Graphs with Specified Degree Sequence / J. F. Lynch 301

Homomorphism Closed vs. Existential Positive / T. Feder, M. Y. Vardi 311

Tractable Conservative Constraint Satisfaction Problems / A. A. Bulatov 321

A Constraint-Based Presentation and Generalization of Rows / F. Pottier 331

Labelled Markov Processes: Stronger and Faster Approximations / V. Danos, J. Desharnais 341

Model Checking for Probability and Time: From Theory to Practice / M. Kwiatkowska 351

Model Checking Guarded Protocols / E. A. Emerson, V. Kahlon 361

Model-Checking Trace Event Structures / P. Madhusudan 371

Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems / N. Piterman, M. Y. Vardi 381

A Proposal to Extend Abstract State Machines to Applications in Systems Biology / J. F. Lynch

Stuttering Refinement on Partial Systems / S. Nejati, A. Gurfinkel

Assume-Guarantee Reasoning with Features / B. Devereux

Modularity Theorems for Non-Monotone Induction / M. Denecker, E. Ternovska

Linear-Time Algorithms for Monadic Logic / S. Lindell

Game-Based Notions of Locality / M. Arenas, P. Barcelo, L. Libkin

Arb: An Implementation of Selecting Tree Automata for XML Query Processing / M. Grohe, C. Koch.

Notes:

"IEEE Computer Society Order Number PR01884"--T.p. verso.

Includes bibliographical references and author index.

ISBN:

0769518842

9780769518848

OCLC:

52570071

Access Restriction:

Restricted for use by site license.