Inhaltsverzeichnis
Invited Lectures. - Notions of Average-Case Complexity for Random 3-SAT. - Abstract Interpretation of Proofs: Classical Propositional Calculus. - Applications of Craig Interpolation to Model Checking. - Bindings, Mobility of Bindings, and the ? -Quantifier: An Abstract. - My (Un)Favourite Things. - Regular Papers. - On Nash Equilibria in Stochastic Games. - A Bounding Quantifier. - Parity and Exploration Games on Infinite Graphs. - Integrating Equational Reasoning into Instantiation-Based Theorem Proving. - Goal-Directed Methods for ? ukasiewicz Logic. - A General Theorem on Termination of Rewriting. - Predicate Transformers and Linear Logic: Yet Another Denotational Model. - Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity. - On Proof Nets for Multiplicative Linear Logic with Units. - The Boundary Between Decidability and Undecidability for Transitive-Closure Logics. - Game-Based Notions of Locality Over Finite Models. - Fixed Points of Type Constructors and Primitive Recursion. - On the Building of Affine Retractions. - Higher-Order Matching in the Linear ? -calculus with Pairing. - A Dependent Type Theory with Names and Binding. - Towards Mechanized Program Verification with Separation Logic. - A Functional Scenario for Bytecode Verification of Resource Bounds. - Proving Abstract Non-interference. - Intuitionistic LTL and a New Characterization of Safety and Liveness. - Moving in a Crumbling Network: The Balanced Case. - Parameterized Model Checking of Ring-Based Message Passing Systems. - A Third-Order Bounded Arithmetic Theory for PSPACE. - Provably Total Primitive Recursive Functions: Theories with Induction. - Logical Characterizations of PSPACE. - The Logic of the Partial ? -Calculus with Equality. - Complete Lax Logical Relations for Cryptographic Lambda-Calculi. -Subtyping Union Types. - Pfaffian Hybrid Systems. - Axioms for Delimited Continuations in the CPS Hierarchy. - Set Constraints on Regular Terms. - Unsound Theorem Proving. - A Space Efficient Implementation of a Tableau Calculus for a Logic with a Constructive Negation. - Automated Generation of Analytic Calculi for Logics with Linearity.
