Proceedings of the 18th IEEE Symposium on Logic in Computer Science
LICS, 2003.

@proceedings{LICS-2003,
	address       = "Ottawa, Canada",
	ee            = "http://www.computer.org/csdl/proceedings/lics/2003/1884/00/index.html",
	isbn          = "0-7695-1884-2",
	publisher     = "{IEEE Computer Society}",
	title         = "{Proceedings of the 18th IEEE Symposium on Logic in Computer Science}",
	year          = 2003,
}

Contents (39 items)

6 ×#logic
4 ×#proving
3 ×#decidability
3 ×#model checking
2 ×#constraints
2 ×#generative
2 ×#linear
2 ×#on the
2 ×#process
2 ×#protocol

LICS-2003-HughesG #linear #logic #multi #proving

Proof Nets for Unit-free Multiplicative-Additive Linear Logic (DJDH, RJvG), pp. 1–10.

LICS-2003-LaurentR #linear #logic

About Translations of Classical Logic into Polarized Linear Logic (OL, LR), pp. 11–20.

LICS-2003-Raffalli

System ST β-reduction and completeness (CR), p. 21–?.

LICS-2003-Pierce #generative #programming language

Types and Programming Languages: The Next Generation (BCP), p. 32–?.

LICS-2003-AhmedJW #reasoning

Reasoning about Hierarchical Storage (AJA, LJ, DW), pp. 33–44.

LICS-2003-Harrison #verification

Formal Verification at Intel (JH), p. 45–?.

LICS-2003-GanzingerK #proving #theorem proving

New Directions in Instantiation-Based Theorem Proving (HG, KK), pp. 55–64.

LICS-2003-DershowitzK

Abstract Saturation-Based Inference (ND, CK), pp. 65–74.

LICS-2003-KorovinV #order

Orienting Equalities with the Knuth-Bendix Order (KK, AV), p. 75–?.

LICS-2003-Kopylov #type system

Dependent Intersection: A New Way of Defining Records in Type Theory (AK), pp. 86–95.

LICS-2003-KuncakR #decidability #recursion #type system

Structural Subtyping of Non-Recursive Types is Decidable (VK, MCR), pp. 96–107.

LICS-2003-Murawski #equivalence #on the

On Program Equivalence in Languages with Ground-Type References (ASM), p. 108–?.

LICS-2003-MillerT #proving

A Proof Theory for Generic Judgments: An extended abstract (DM, AFT), pp. 118–127.

LICS-2003-Oliva #algorithm #effectiveness #polynomial #proving

Polynomial-time Algorithms from Ineffective Proofs (PO), pp. 128–137.

LICS-2003-Buresh-OppenheimP #complexity

The Complexity of Resolution Refinements (JBO, TP), p. 138–?.

LICS-2003-Rossman #finite

Successor-Invariance in the Finite (BR), p. 148–?.

LICS-2003-GradelK #fixpoint

Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions (EG, SK), p. 158–?.

LICS-2003-KhoussainovRS #automation #on the #partial order

On Automatic Partial Orders (BK, SR, FS), pp. 168–177.

LICS-2003-LibkinN #logic #query

Logical Definability and Query Languages over Unranked Trees (LL, FN), pp. 178–187.

LICS-2003-FrickGK #evaluation #query

Query Evaluation on Compressed Trees (MF, MG, CK), p. 188–?.

LICS-2003-OuaknineW #automaton #decidability #robust

Revisiting Digitization, Robustness, and Decidability for Timed Automata (JO, JW), pp. 198–207.

LICS-2003-Drimmelen #logic #satisfiability

Satisfiability in Alternating-time Temporal Logic (GvD), pp. 208–217.

LICS-2003-Jancar #parallel #process #similarity

Strong Bisimilarity on Basic Parallel Processes is PSPACE-complete (PJ), p. 218–?.

LICS-2003-Abadi #data access #logic

Logic in Access Control (MA), p. 228–?.

LICS-2003-PistoreV #infinity

The Planning Spectrum — One, Two, Three, Infinity (MP, MYV), pp. 234–243.

LICS-2003-McCarthy #logic

Advice about logical AI (JM), p. 244–?.

LICS-2003-NeculaS #framework #generative

A Sound Framework for Untrusted Verification-Condition Generators (GCN, RRS), pp. 248–260.

LICS-2003-ChevalierKRT #protocol

An NP Decision Procedure for Protocol Insecurity with XOR (YC, RK, MR, MT), pp. 261–270.

LICS-2003-Comon-LundhS #constraints #deduction #theorem proving

Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or (HCL, VS), p. 271–?.

LICS-2003-Hunter

Spectrum Hierarchies and Subdiagonal Functions (AH), pp. 281–290.

LICS-2003-GurevichS #higher-order #monad

Spectra of Monadic Second-Order Formulas with One Unary Function (YG, SS), pp. 291–300.

LICS-2003-Lynch #convergence #graph #random #sequence

Convergence Law for Random Graphs with Specified Degree Sequence (JFL), p. 301–?.

LICS-2003-FederV #morphism

Homomorphism Closed vs. Existential Positive (TF, MYV), pp. 311–320.

LICS-2003-Bulatov #constraints #problem

Tractable conservative Constraint Satisfaction Problems (AAB), p. 321–?.

LICS-2003-DanosD #approximate #markov #performance #process

Labelled Markov Processes: Stronger and Faster Approximations (VD, JD), pp. 341–350.

LICS-2003-Kwiatkowska #model checking #probability #theory and practice

Model checking for probability and time: from theory to practice (MZK), p. 351–?.

LICS-2003-EmersonK #model checking #protocol

Model Checking Guarded Protocols (EAE, VK), pp. 361–370.

LICS-2003-Madhusudan #model checking

Model-checking Trace Event Structures (PM), pp. 371–380.

LICS-2003-PitermanV #decidability #future of #stack

Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems (NP, MYV), p. 381–?.