Invited Lectures -- Full Completeness: Interactive and Geometric Characterizations of the Space of Proofs (Abstract) -- The Symbolic Approach to Repeated Games (Abstract) -- Proofs, Programs and Abstract Complexity -- Model-Checking First-Order Logic: Automata and Locality -- Tightening the Exchange Rates Between Automata -- Precise Relational Invariants Through Strategy Iteration -- Logic and Games -- Omega-Regular Half-Positional Winning Conditions -- Clique-Width and Parity Games -- Logical Refinements of Church’s Problem -- The Power of Counting Logics on Restricted Classes of Finite Structures -- Expressiveness -- Comparing the Expressive Power of Well-Structured Transition Systems -- There Exist Some ?-Powers of Any Borel Rank -- Games and Trees -- Satisfiability of a Spatial Logic with Tree Variables -- Forest Expressions -- MSO on the Infinite Binary Tree: Choice and Order -- Logic and Deduction -- Classical and Intuitionistic Logic Are Asymptotically Identical -- Qualitative Temporal and Spatial Reasoning Revisited -- On Acyclic Conjunctive Queries and Constant Delay Enumeration -- Integrating Linear Arithmetic into Superposition Calculus -- Lambda Calculus 1 -- The Theory of Calculi with Explicit Substitutions Revisited -- A Soft Type Assignment System for ?-Calculus -- Lambda Theories of Effective Lambda Models -- Typed Normal Form Bisimulation -- Lambda Calculus 2 -- Not Enough Points Is Enough -- Classical Program Extraction in the Calculus of Constructions -- Building Decision Procedures in the Calculus of Inductive Constructions -- Finite Model Theory -- Structure Theorem and Strict Alternation Hierarchy for FO2 on Words -- On the Complexity of Reasoning About Dynamic Policies -- Relativizing Small Complexity Classes and Their Theories -- Subexponential Time and Fixed-Parameter Tractability: Exploiting the Miniaturization Mapping -- Linear Logic -- From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic -- Linear Realizability -- Correctness of Multiplicative (and Exponential) Proof Structures is NL-Complete -- Focusing and Polarization in Intuitionistic Logic -- Proof Theory -- Incorporating Tables into Proofs -- A Cut-Free and Invariant-Free Sequent Calculus for PLTL -- Unbounded Proof-Length Speed-Up in Deduction Modulo -- Propositional Logic for Circuit Classes -- Game Characterizations and the PSPACE-Completeness of Tree Resolution Space -- Game Semantics -- Continuous Previsions -- Bad Variables Under Control -- A Games Model of Bunched Implications -- The Ackermann Award 2007.