Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science
LICS, 2000.

@proceedings{LICS-2000,
	address       = "Santa Barbara, California, USA",
	ee            = "http://www.computer.org/csdl/proceedings/lics/2000/0725/00/index.html",
	isbn          = "0-7695-0725-5",
	publisher     = "{IEEE Computer Society}",
	title         = "{Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science}",
	year          = 2000,
}

Contents (39 items)

5 ×#logic
4 ×#game studies
3 ×#algebra
3 ×#first-order
3 ×#performance
3 ×#process
3 ×#proving
2 ×#approximate
2 ×#axiom
2 ×#calculus

LICS-2000-Fagin #complexity #game studies #logic

Logic, Complexity, and Games (RF), p. 3.

LICS-2000-Birkedal

A General Notion of Realizability (LB), pp. 7–17.

LICS-2000-Miquel #type system

A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping (AM), pp. 18–29.

LICS-2000-SimpsonP #axiom #category theory #fixpoint

Complete Axioms for Categorical Fixed-Point Operators (AKS, GDP), pp. 30–41.

LICS-2000-LindellW #decidability #finite #first-order

The Role of Decidability in First Order Separations over Classes of Finite Structures (SL, SW), pp. 45–50.

LICS-2000-BlumensathG #automation

Automatic Structures (AB, EG), pp. 51–62.

LICS-2000-AfratiLR

Definability and Compression (FNA, HL, MdR), pp. 63–73.

LICS-2000-BussK #bound

Resource-Bounded Continuity and Sequentiality for Type-Two Functionals (SRB, BMK), pp. 77–83.

LICS-2000-AehligS #analysis #polynomial

A Syntactical Analysis of Non-Size-Increasing Polynomial Time Computation (KA, HS), pp. 84–91.

LICS-2000-DesharnaisGJP #approximate #markov #process

Approximating Labeled Markov Processes (JD, VG, RJ, PP), pp. 95–106.

LICS-2000-BloomFG

Precongruence Formats for Decorated Trace Preorders (BB, WF, RJvG), pp. 107–118.

LICS-2000-EmersonHT #reduction #symmetry

Virtual Symmetry Reduction (EAE, JH, RJT), pp. 121–131.

LICS-2000-AbdullaN #infinity #performance #verification

Better is Better than Well: On Efficient Verification of Infinite-State Systems (PAA, AN), pp. 132–140.

LICS-2000-AlfaroH #concurrent #game studies

Concurrent ω-Regular Games (LdA, TAH), pp. 141–154.

LICS-2000-LemstromH #approximate #logic #pattern matching #transitive

Approximate Pattern Matching is Expressible in Transitive Closure Logic (KL, LH), pp. 157–167.

LICS-2000-BergmanS #algebra #complexity #problem

Computational Complexity of Some Problems Involving Congruences on Algebras (CB, GS), pp. 168–174.

LICS-2000-Kripke #algorithm #first-order #theorem

From the Church-Turing Thesis to the First-Order Algorithm Theorem (SK), p. 177.

LICS-2000-Selman #challenge #problem #satisfiability #testing

Satisfiability Testing: Recent Developments and Challenge Problems (BS), p. 178.

LICS-2000-MurawskiO #performance #proving #verification

Dominator Trees and Fast Verification of Proof Nets (ASM, CHLO), pp. 181–191.

LICS-2000-Chroboczek #game studies #semantics #type system

Game Semantics and Subtyping (JC), pp. 192–203.

LICS-2000-DanosH #game studies #probability #semantics

Probabilistic Game Semantics (VD, RH), pp. 204–213.

LICS-2000-GradelHO #logic

Back and Forth between Guarded and Modal Logics (EG, CH, MO), pp. 217–228.

LICS-2000-Reynolds

More Past Glories (MR), pp. 229–240.

LICS-2000-Moszkowski #axiom #infinity #logic

A Complete Axiomatization of Interval Temporal Logic with Infinite Time (BCM), pp. 241–252.

LICS-2000-Nakano #recursion

A Modality for Recursion (HN), pp. 255–266.

LICS-2000-Prost #calculus #dependence

A Static Calculus of Dependencies for the λ-Cube (FP), pp. 267–276.

LICS-2000-RybinaV #algebra

A Decision Procedure for Term Algebras with Queues (TR, AV), pp. 279–290.

LICS-2000-KorovinV #algebra

A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering (KK, AV), pp. 291–302.

LICS-2000-McMillan #model checking #proving #theorem

Some Strategies for Proving Theorems with a Model Checker (KLM), pp. 305–306.

LICS-2000-Krivine #set

The Curry-Howard Correspondence in Set Theory (JLK), pp. 307–308.

LICS-2000-JeffreyR #bisimulation #concurrent #formal method #ml

A Theory of Bisimulation for a Fragment of Concurrent ML with Local Names (AJ, JR), pp. 311–321.

LICS-2000-CattaniS #modelling #process

Models for Name-Passing Processes: Interleaving and Causal (GLC, PS), pp. 322–333.

LICS-2000-YoshidaH #process

Assigning Types to Processes (NY, MH), pp. 334–345.

LICS-2000-GroheS #first-order #on the #query

On First-Order Topological Queries (MG, LS), pp. 349–360.

LICS-2000-CalvaneseGLV #constraints #query

View-Based Query Processing and Constraint Satisfaction (DC, GDG, ML, MYV), pp. 361–371.

LICS-2000-Xi #dependent type #imperative #programming

Imperative Programming with Dependent Types (HX), pp. 375–387.

LICS-2000-PalsbergZ #flexibility #performance #recursion

Efficient and Flexible Matching of Recursive Types (JP, TZ), pp. 388–398.

LICS-2000-Voronkov #calculus #how #logic #proving

How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi (AV), pp. 401–412.

LICS-2000-GodoyN

Paramodulation with Built-in Abelian Groups (GG, RN), pp. 413–424.