15. CSL 2001: Paris, France

Invited Papers

• Peter W. O'Hearn, John C. Reynolds, Hongseok Yang:
  Local Reasoning about Programs that Alter Data Structures. 1-19
  
• Jan Van den Bussche:
  Applications of Alfred Tarski's Ideas in Database Theory. 20-37
  
• Jean-Yves Girard:
  Locus Solum: From the Rules of Logic to the Logic of Rules. 38
  

Contributed Papers

• Max I. Kanovich:
  The Expressive Power of Horn Monadic Linear Logic. 39-53
  
• Alessio Guglielmi, Lutz Straßburger:
  Non-commutativity and MELL in the Calculus of Structures. 54-68
  
• Virgile Mogbil:
  Quadratic Correctness Criterion for Non-commutative Logic. 69-83
  

Descriptive Complexity

• Yijia Chen, Enshao Shen:
  Capture Complexity by Partition. 84-98
  
• Martin Grohe, Stefan Wöhrle:
  An Existential Locality Theorem. 99-114
  
• Jean-Yves Marion:
  Actual Arithmetic and Feasibility. 115-129
  
• Nicole Schweikardt:
  The Natural Order-Generic Collapse for omega-Representable Databases over the Rational and the Real Ordered Group. 130-144
  

Semantics

• John Power, Konstantinos Tourlas:
  An Algebraic Foundation for Higraphs. 145-159
  
• Margarita V. Korovina, Oleg V. Kudinov:
  Semantic Characterisations of Second-Order Computability over the Real Numbers. 160-172
  
• Edmund Robinson, Giuseppe Rosolini:
  An Abstract Look at Realizability. 173-187
  
• Vincent Danos, Russell Harmer:
  The Anatomy of Innocence. 188-202
  

Higher-Order Programs

• Marc Bezem:
  An Improved Extensionality Criterion for Higher-Order Logic Programs. 203-216
  
• Robert F. Stärk, Stanislas Nanchen:
  A Logic for Abstract State Machines. 217-231
  
• Jan van Eijck:
  Constrained Hyper Tableaux. 232-246
  

Modal Logics

• Carsten Lutz, Ulrike Sattler, Frank Wolter:
  Modal Logic and the Two-Variable Fragment. 247-261
  
• Frédéric Koriche:
  A Logic for Approximate First-Order Reasoning. 262-276
  
• Anuj Dawar, Erich Grädel, Stephan Kreutzer:
  Inflationary Fixed Points in Modal Logic. 277-291
  
• Natasha Alechina, Michael Mendler, Valeria de Paiva, Eike Ritter:
  Categorical and Kripke Semantics for Constructive S4 Modal Logic. 292-307
  

Verification

• Thomas Marthedal Rasmussen:
  Labelled Natural Deduction for Interval Logics. 308-323
  
• Frank S. de Boer, Rogier M. van Eijk:
  Decidable Navigation Logics for Object Structures. 324-338
  
• Witold Charatonik, Jean-Marc Talbot:
  The Decidability of Model Checking Mobile Ambients. 339-354
  

Automata

• Matthias Galota, Heribert Vollmer:
  A Generalization of the Büchi-Elgot-Trakhtenbrot Theorem. 355-368
  
• Olivier Finkel:
  An Effective Extension of the Wagner Hierarchy to Blind Counter Automata. 369-383
  
• Felix Klaedtke:
  Decision Procedure for an Extension of WS1S. 384-398
  

Lambda-Calculus

• Yohji Akama:
  Limiting Partial Combinatory Algebras towards Infinitary Lambda-Calculi and Classical Logic. 399-413
  
• Simona Ronchi Della Rocca, Luca Roversi:
  Intersection Logic. 414-428
  
• Lutz Schröder:
  Life without the Terminal Type. 429-442
  
• Samson Abramsky, Marina Lenisa:
  Fully Complete Minimal PER Models for the Simply Typed lambda-Calculus. 443-457
  

Induction

• Keye Martin:
  A Principle of Induction. 458-468
  
• Matthias Baaz, Georg Moser:
  On a Generalisation of Herbrand's Theorem. 469-483
  
• Jean Goubault-Larrecq:
  Well-Founded Recursive Relations. 484-497
  

Equational Calculus

• Manfred Schmidt-Schauß:
  Stratified Context Unification Is in PSPACE. 498-512
  
• Alessandro Armando, Silvio Ranise, Michaël Rusinowitch:
  Uniform Derivation of Decision Procedures by Superposition. 513-527
  
• Grigore Rosu:
  Complete Categorical Equational Deduction. 528-538
  
• Hitoshi Ohsaki:
  Beyond Regularity: Equational Tree Automata for Associative and Commutative Theories. 539-553
  

Constructive Theory of Types

• Pierre Courtieu:
  Normalized Types. 554-569
  
• Alexei Kopylov, Aleksey Nogin:
  Markov's Principle for Propositional Type Theory. 570-584
  
• Carsten Schürmann:
  Recursion for Higher-Order Encodings. 585-599
  
• Ralph Matthes:
  Monotone Inductive and Coinductive Constructors of Rank 2. 600-614