18. CSL 2004: Karpacz, Poland

Invited Lectures

• Albert Atserias:
  Notions of Average-Case Complexity for Random 3-SAT. 1-5
  
• Martin Hyland:
  Abstract Interpretation of Proofs: Classical Propositional Calculus. 6-21
  
• Kenneth L. McMillan:
  Applications of Craig Interpolation to Model Checking. 22-23
  
• Dale Miller:
  Bindings, Mobility of Bindings, and the "generic judgments"-Quantifier: An Abstract. 24
  
• Pawel Urzyczyn:
  My (Un)Favourite Things. 25
  

Regular Papers

• Krishnendu Chatterjee, Rupak Majumdar, Marcin Jurdzinski:
  On Nash Equilibria in Stochastic Games. 26-40
  
• Mikolaj Bojanczyk:
  A Bounding Quantifier. 41-55
  
• Hugo Gimbert:
  Parity and Exploration Games on Infinite Graphs. 56-70
  
• Harald Ganzinger, Konstantin Korovin:
  Integrating Equational Reasoning into Instantiation-Based Theorem Proving. 71-84
  
• George Metcalfe, Nicola Olivetti, Dov M. Gabbay:
  Goal-Directed Methods for Lukasiewicz Logic. 85-99
  
• Jeremy E. Dawson, Rajeev Goré:
  A General Theorem on Termination of Rewriting. 100-114
  
• Pierre Hyvernat:
  Predicate Transformers and Linear Logic: Yet Another Denotational Model. 115-129
  
• Pietro Di Gianantonio:
  Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity. 130-144
  
• Lutz Straßburger, François Lamarche:
  On Proof Nets for Multiplicative Linear Logic with Units. 145-159
  
• Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh:
  The Boundary Between Decidability and Undecidability for Transitive-Closure Logics. 160-174
  
• Marcelo Arenas, Pablo Barceló, Leonid Libkin:
  Game-Based Notions of Locality Over Finite Models. 175-189
  
• Andreas Abel, Ralph Matthes:
  Fixed Points of Type Constructors and Primitive Recursion. 190-204
  
• Aleksy Schubert:
  On the Building of Affine Retractions. 205-219
  
• Philippe de Groote, Sylvain Salvati:
  Higher-Order Matching in the Linear lambda-calculus with Pairing. 220-234
  
• Ulrich Schöpp, Ian Stark:
  A Dependent Type Theory with Names and Binding. 235-249
  
• Tjark Weber:
  Towards Mechanized Program Verification with Separation Logic. 250-264
  
• Roberto M. Amadio, Solange Coupet-Grimal, Silvano Dal-Zilio, Line Jakubiec:
  A Functional Scenario for Bytecode Verification of Resource Bounds. 265-279
  
• Roberto Giacobazzi, Isabella Mastroeni:
  Proving Abstract Non-interference. 280-294
  
• Patrick Maier:
  Intuitionistic LTL and a New Characterization of Safety and Liveness. 295-309
  
• Philipp Rohde:
  Moving in a Crumbling Network: The Balanced Case. 310-324
  
• E. Allen Emerson, Vineet Kahlon:
  Parameterized Model Checking of Ring-Based Message Passing Systems. 325-339
  
• Alan Skelley:
  A Third-Order Bounded Arithmetic Theory for PSPACE. 340-354
  
• Andrés Cordón-Franco, Alejandro Fernández-Margarit, Francisco Félix Lara Martín:
  Provably Total Primitive Recursive Functions: Theories with Induction. 355-369
  
• David Richerby:
  Logical Characterizations of PSPACE. 370-384
  
• Lutz Schröder:
  The Logic of the Partial lambda-Calculus with Equality. 385-399
  
• Jean Goubault-Larrecq, Slawomir Lasota, David Nowak, Yu Zhang:
  Complete Lax Logical Relations for Cryptographic Lambda-Calculi. 400-414
  
• Jerome Vouillon:
  Subtyping Union Types. 415-429
  
• Margarita V. Korovina, Nicolai Vorobjov:
  Pfaffian Hybrid Systems. 430-441
  
• Yukiyoshi Kameyama:
  Axioms for Delimited Continuations in the CPS Hierarchy. 442-457
  
• Pawel Rychlikowski, Tomasz Truderung:
  Set Constraints on Regular Terms. 458-472
  
• Christopher Lynch:
  Unsound Theorem Proving. 473-487
  
• Alessandro Avellone, Camillo Fiorentini, Guido Fiorino, Ugo Moscato:
  A Space Efficient Implementation of a Tableau Calculus for a Logic with a Constructive Negation. 488-502
  
• Agata Ciabattoni:
  Automated Generation of Analytic Calculi for Logics with Linearity. 503-517