Computer Science Logic: 15th International Workshop, CSL 2001 10th Annual Conference of the EACSL Paris, France, September 10–13, 2001, Proceedings

Peter O’Hearn, John Reynolds, Hongseok Yang (auth.), Laurent Fribourg (eds.)3540425543, 9783540425540

This book constitutes the refereed proceedings of the 15th International Workshop on Computer Science Logic, CSL 2001, held as the 10th Annual Conerence of the EACSL in Paris, France in September 2001.
The 39 revised full papers presented together with two invited papers were carefully reviewed and selected from 91 submissions. The papers are organized in topical sections on linear logic, descriptive complexity, semantics, higher-order programs, model logics, verification, automata, lambda calculus, induction, equational calculus, and constructive theory of types.

---

Table of contents :
Local Reasoning about Programs that Alter Data Structures….Pages 1-19
Applications of Alfred Tarski’s Ideas in Database Theory….Pages 20-37
Locus Solum: From the Rules of Logic to the Logic of Rules….Pages 38-38
The Expressive Power of Horn Monadic Linear Logic….Pages 39-53
Non-commutativity and MELL in the Calculus of Structures….Pages 54-68
Quadratic Correctness Criterion for Non-commutative Logic….Pages 69-83
Capture Complexity by Partition….Pages 84-98
An Existential Locality Theorem….Pages 99-114
Actual Arithmetic and Feasibility….Pages 115-129
The Natural Order-Generic Collapse for ω -Representable Databases over the Rational and the Real Ordered Group….Pages 130-144
An Algebraic Foundation for Higraphs….Pages 145-159
Semantic Characterisations of Second-Order Computability over the Real Numbers….Pages 160-172
An Abstract Look at Realizability….Pages 173-187
The Anatomy of Innocence….Pages 188-202
An Improved Extensionality Criterion for Higher-Order Logic Programs….Pages 203-216
A Logic for Abstract State Machines….Pages 217-231
Constrained Hyper Tableaux….Pages 232-246
Modal Logic and the Two-Variable Fragment….Pages 247-261
A Logic for Approximate First-Order Reasoning….Pages 262-276
Inflationary Fixed Points in Modal Logic….Pages 277-291
Categorical and Kripke Semantics for Constructive S4 Modal Logic….Pages 292-307
Labelled Natural Deduction for Interval Logics….Pages 308-323
Decidable Navigation Logics for Object Structures….Pages 324-338
The Decidability of Model Checking Mobile Ambients….Pages 339-354
A Generalization of the Büchi-Elgot-Trakhtenbrot Theorem….Pages 355-368
An Effective Extension of the Wagner Hierarchy to Blind Counter Automata….Pages 369-383
Decision Procedure for an Extension of WS1S….Pages 384-398
Limiting Partial Combinatory Algebras towards Infinitary Lambda-Calculi and Classical Logic….Pages 399-414
Intersection Logic….Pages 414-429
Life without the Terminal Type….Pages 429-442
Fully Complete Minimal PER Models for the Simply Typed λ-Calculus….Pages 443-457
A Principle of Induction….Pages 458-468
On a Generalisation of Herbrand’s Theorem….Pages 469-483
Well-Founded Recursive Relations….Pages 484-498
Stratified Context Unification Is in PSPACE….Pages 498-513
Uniform Derivation of Decision Procedures by Superposition….Pages 513-527
Complete Categorical Equational Deduction….Pages 528-538
Beyond Regularity: Equational Tree Automata for Associative and Commutative Theories….Pages 539-553
Normalized Types….Pages 554-569
Markov’s Principle for Propositional Type Theory….Pages 570-584
Recursion for Higher-Order Encodings….Pages 585-599
Monotone Inductive and Coinductive Constructors of Rank 2….Pages 600-614