Computer Science Logic: 13th International Workshop, CSL’99 8th Annual Conference of the EACSL Madrid, Spain, September 20–25, 1999 Proceedings

Victor Vianu (auth.), Jörg Flum, Mario Rodriguez-Artalejo (eds.)3540665366, 9783540665366

The 1999 Annual Conference of the European Association for Computer Science Logic, CSL’99, was held in Madrid, Spain, on September 20-25, 1999. CSL’99 was the 13th in a series of annual meetings, originally intended as Internat- nal Workshops on Computer Science Logic, and the 8th to be held as the – nual Conference of the EACSL. The conference was organized by the Computer Science Departments (DSIP and DACYA) at Universidad Complutense in M- rid (UCM). The CSL’99 program committee selected 34 of 91 submitted papers for p- sentation at the conference and publication in this proceedings volume. Each submitted paper was refereed by at least two, and in almost all cases, three di erent referees. The second refereeing round, previously required before a – per was accepted for publication in the proceedings, was dropped following a decision taken by the EACSL membership meeting held during CSL’98 (Brno, Czech Republic, August 25, 1998).

---

Table of contents :
Topological Queries in Spatial Databases….Pages 1-1
The Consistency Dimension, Compactness, and Query Learning….Pages 2-13
Descriptive and Parameterized Complexity….Pages 14-31
Logical Specification of Operational Semantics….Pages 32-49
Constraint-Based Analysis of Broadcast Protocols….Pages 50-66
Using Fields and Explicit Substitutions to Implement Objects and Functions in a de Bruijn Setting….Pages 204-219
Closed Reductions in the λ-Calculus….Pages 220-234
Kripke Resource Models of a Dependently-Typed, Bunched λ-Calculus (Extended Abstract)….Pages 235-249
A Linear Logical View of Linear Type Isomorphisms….Pages 250-265
Choice Logic Programs and Nash Equilibria in Strategic Games….Pages 266-276
Resolution Method for Modal Logic with Well-Founded Frames….Pages 277-291
Descriptive Complexity Theory for Constraint Databases….Pages 67-81
Applicative Control and Computational Complexity….Pages 82-95
Applying Rewriting Techniques to the Verification of Erlang Processes….Pages 96-110
Difference Decision Diagrams….Pages 111-125
Analysis of Hybrid Systems: An Ounce of Realism Can Save an Infinity of States….Pages 126-139
Verifying Liveness by Augmented Abstraction….Pages 141-156
Signed Interval Logic….Pages 157-171
Quantitative Temporal Logic….Pages 172-187
An Expressively Complete Temporal Logic without Past Tense Operators for Mazurkiewicz Traces….Pages 188-203
A Universal Innocent Game Model for the Böhm Tree Lambda Theory….Pages 405-419
Anti-Symmetry of Higher-Order Subtyping….Pages 420-438
Safe Proof Checking in Type Theory with Y ….Pages 439-452
Monadic Presentations of Lambda Terms Using Generalized Inductive Types….Pages 453-468
A P-Time Completeness Proof for Light Logics….Pages 469-483
On Guarding Nested Fixpoints….Pages 484-498
A Logical Viewpoint on Process-Algebraic Quotients….Pages 499-514
A Truly Concurrent Semantics for a Simple Parallel Programming Language….Pages 515-529
A NExpTime-Complete Description Logic Strictly Contained in C 2 ….Pages 292-306
A Road-Map on Complexity for Hybrid Logics….Pages 307-321
Specification Refinement with System F….Pages 530-545
Pre-logical Relations….Pages 546-561
Data-Refinement for Call-By-Value Programming Languages….Pages 562-576
MonadicNLIN and Quantifier-Free Reductions….Pages 322-337
Directed Reachability: From Ajtai-Fagin to Ehrenfeucht-Fraïssé Games….Pages 338-349
Fixpoint Alternation and the Game Quantifier….Pages 350-361
Lower Bounds for Space in Resolution….Pages 362-373
Program Schemes, Arrays, Lindström Quantifiers and Zero-One Laws….Pages 374-388
Open Least Element Principle and Bounded Query Computation….Pages 389-404
Tutorial on Term Rewriting….Pages 577-577
Tutorial on Interactive Theorem Proving Using Type Theory….Pages 578-578