"Computer Science Logic" ed. by Jerzy Marcinkowski, Andrzej Tarlecki

The 33 revised full papers presented together with 5 invited contributions were carefully reviewed and selected from 88 papers submitted. All current aspects of logic in computer science are addressed ranging from mathematical logic and logical foundations to methodological issues and applications of logics in various computing contexts.





Table of Contents
Invited Lectures
Notions of Average-Case Complexity for Random 3-SAT - Albert Atserias
Abstract Interpretation of Proofs: Classical Propositional Calculus - Martin Hyland
Applications of Craig Interpolation to Model Checking - Kenneth McMillan
Bindings, Mobility of Bindings, and the An Abstract - Dale Miller
My (Un)Favourite Things
Regular Papers
On Nash Equilibria in Stochastic Games - Krishnendu Chatterjee, Rupak Majumdar
A Bounding Quantifier
Parity and Exploration Games on Infinite Graphs - Hugo Gimbert
Integrating Equational Reasoning into Instantiation-Based Theorem Proving - Harald Ganzinger, Konstantin Korovin
Goal-Directed Methods for Logic - George Metcalfe, Nicola Olivetti, Dov Gabbay
A General Theorem on Termination of Rewriting - Jeremy E. Dawson, Rajeev Goré
Predicate Transformers and Linear Logic: Yet Another Denotational Model - Pierre Hyvernat
Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity - Pietro Di Gianantonio
On Proof Nets for Multiplicative Linear Logic with Units - Lutz Straßburger, François Lamarche
The Boundary Between Decidability and Undecidability for Transitive-Closure Logics - Neil Immerman, Alex Rabinovich, Tom Reps, Mooly Sagiv, Greta Yorsh
Game-Based Notions of Locality over Finite Models - Marcelo Arenas, Pablo Barceló, Leonid Libkin
Fixed Points of Type Constructors and Primitive Recursion - Andreas Abel, Ralph Matthes
On the Building of Affine Retractions - Aleksy Schubert
Higher-Order Matching in the Linear with Pairing - Philippe de Groote, Sylvain Salvati
A Dependent Type Theory with Names and Binding - Ulrich Schöpp, Ian Stark
Towards Mechanized Program Verification with Separation Logic - Tjark Weber
A Functional Scenario for Bytecode Verification of Resource Bounds - Roberto M. Amadio, Solange Coupet-Grimal, Silvano Dal Zilio, Line Jakubiec
Proving Abstract Non-interference - Roberto Giacobazzi, Isabella Mastroeni
Intuitionistic LTL and a New Characterization of Safety and Liveness - Patrick Maier
Moving in a Crumbling Network: The Balanced Case - Philipp Rohde
Parameterized Model Checking of Ring-Based Message Passing Systems - E. Allen Emerson, Vineet Kahlon
A Third-Order Bounded Arithmetic Theory for PSPACE - Alan Skelley
Provably Total Primitive Recursive Functions: Theories with Induction - Andrés Cordón-Franco, Alejandro Fernández-Margarit, F. Félix Lara-Martín
Logical Characterizations of PSPACE - David Richerby
The Logic of the Partial with Equality - Lutz Schröder
Complete Lax Logical Relations for Cryptographic Lambda-Calculi - Jean Goubault-Larrecq, David Nowak, Yu Zhang
Subtyping Union Types - Jérôme Vouillon
Pfaffian Hybrid Systems - Margarita Korovina and Nicolai Vorobjov
Axioms for Delimited Continuations in the CPS Hierarchy - Yukiyoshi Kameyama
Set Constraints on Regular Terms - and Tomasz Truderung
Unsound Theorem Proving - Christopher Lynch
A Space Efficent Implementation of a Tableau Calculus for a Logic with a Constructive Negation - Alessandro Avellone, Camillo Fiorentini, Guido Fiorino, Ugo Moscato
Automated Generation of Analytic Calculi for Logics with Linearity - Agata Ciabattoni
Author Index