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

by Flum, J.; Artalejo, M. Rodriguez; Goos, G.; Hartmanis, J.; Leeuwen, J. van

• ISBN13: 9783540665366
• ISBN10: 3540665366
• Format: Paperback
• Copyright: 1999-11-01
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the 13th Annual International Conference on Computer Science Logic, CSL '99, held under the sponsorship of EACSL in Madrid, Spain in September 1999.The 34 revised full papers presented together with five invited contributions were carefully reviewed and sleected from a total of 91 submissions. The papers are organized in sections on descriptive complexity; verification; temporal logic; lambda calculus and linear logic; logic programming, modal logic, and description logic; logic and complexity; lambda calculus and type theory; linear logic, mu calculus, and concurrency; and specification and data refinement.

Table of Contents

Invited Papers
Topological Queries in Spatial Databases	p. 1
The Consistency Dimension, Compactness, and Query Learning	p. 2
Descriptive and Parameterized Complexity	p. 14
Logical Specification of Operational Semantics	p. 32
Constraint-Based Analysis of Broadcast Protocols	p. 50
Contributed Papers
Descriptive Complexity, I
Descriptive Complexity Theory for Constraint Databases	p. 67
Applicative Control and Computational Complexity	p. 82
Verification
Applying Rewriting Techniques to the Verification of Erlang Processes	p. 96
Difference Decision Diagrams	p. 111
Analysis of Hybrid Systems: An Ounce of Realism Can Save an Infinity of States	p. 126
Verifying Liveness by Augmented Abstraction	p. 141
Temporal Logic
Signed Interval Logic	p. 157
Quantitative Temporal Logic	p. 172
An Expressively Complete Temporal Logic without Past Tense Operators for Mazurkiewicz Traces	p. 188
Lambda Calculus, Linear Logic
Using Fields and Explicit Substitutions to Implement Objects and Functions in a de Bruijn Setting	p. 204
Closed Reductions in the ¿-Calculus	p. 220
Kripke Resource Models of a Dependently-Typed, Bunched ¿-Calculus	p. 235
A Linear Logical View of Linear Type Isomorphisms	p. 250
Logic Programming, Modal Logic, Description Logic
Choice Logic Programs and Nash Equilibria in Strategic Games	p. 266
Resolution Method for Modal Logic with Well-Founded Frames	p. 277
A NExpTime-Complete Description Logic Strictly Contained in C2	p. 292
A Road-Map on Complexity for Hybrid Logics	p. 307
Descriptive Complexity, II
MonadicNLIN and Quantifier-Free Reductions	p. 322
Directed Reachability: From Ajtai-Fagin to Ehrenfeucht-Fraïssé Games	p. 338
Fixpoint Alternation and the Game Quantifier	p. 350
Logic and Complexity
Lower Bounds for Space in Resolution	p. 362
Program Schemes, Arrays, Lindstrom Quantifiers and Zero-One Laws	p. 374
Open Least Element Principle and Bounded Query Computation	p. 389
Lambda Calculus, Type Theory
A Universal Innocent Game Model for the Bohm Tree Lambda Theory	p. 405
Anti-Symmetry of Higher-Order Subtyping	p. 420
Safe Proof Checking in Type Theory with Y	p. 439
Monadic Presentations of Lambda Terms Using Generalized Inductive Types	p. 453
Linear Logic, Mu Calculus, Concurrency
A P-Time Completeness Proof for Light Logics	p. 469
On Guarding Nested Fixpoints	p. 484
A Logical Viewpoint on Process-Algebraic Quotients	p. 499
A Truly Concurrent Semantics for a Simple Parallel Programming Language	p. 515
Specification, Data Refinement
Specification Refinement with System F	p. 530
Pre-logical Relations	p. 546
Data-Refinement for Call-By-Value Programming Languages	p. 562
Tutorials
Term Rewriting	p. 577
Interactive Theorem Proving Using Type Theory	p. 578
Author Index	p. 579
Table of Contents provided by Publisher. All Rights Reserved.