| 2007 | From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic. | Dale Miller, Alexis Saurin |
| 2007 | Incorporating Tables into Proofs. | Dale Miller, Vivek Nigam |
| 2007 | A Games Model of Bunched Implications. | Guy McCusker, David J. Pym |
| 2007 | Focusing and Polarization in Intuitionistic Logic. | Chuck C. Liang, Dale Miller |
| 2007 | Typed Normal Form Bisimulation. | Sren B. Lassen, Paul Blain Levy |
| 2007 | Tightening the Exchange Rates Between Automata. | Orna Kupferman |
| 2007 | Integrating Linear Arithmetic into Superposition Calculus. | Konstantin Korovin, Andrei Voronkov |
| 2007 | Omega-Regular Half-Positional Winning Conditions. | Eryk Kopczynski |
| 2007 | The Theory of Calculi with Explicit Substitutions Revisited. | Delia Kesner |
| 2007 | Linear Realizability. | Naohiko Hoshino |
| 2007 | Game Characterizations and the PSPACE-Completeness of Tree Resolution Space. | Alexander Hertel, Alasdair Urquhart |
| 2007 | The Ackermann Award 2007. | Martin Grohe, Martin Hyland, Johann A. Makowsky, Damian Niwinski |
| 2007 | Continuous Previsions. | Jean Goubault-Larrecq |
| 2007 | On the Complexity of Reasoning About Dynamic Policies. | Stefan Gller |
| 2007 | Precise Relational Invariants Through Strategy Iteration. | Thomas Gawlitza, Helmut Seidl |
| 2007 | A Cut-Free and Invariant-Free Sequent Calculus for PLTL. | Joxe Gaintzarain, Montserrat Hermo, Paqui Lucio, Marisa Navarro, Fernando Orejas |
| 2007 | A Soft Type Assignment System for | Marco Gaboardi, Simona Ronchi Della Rocca |
| 2007 | Classical and Intuitionistic Logic Are Asymptotically Identical. | Herv Fournier, Danile Gardy, Antoine Genitrini, Marek Zaionc |
| 2007 | There Exist Some | Olivier Finkel, Dominique Lecomte |
| 2007 | Satisfiability of a Spatial Logic with Tree Variables. | Emmanuel Filiot, Jean-Marc Talbot, Sophie Tison |
| 2007 | The Power of Counting Logics on Restricted Classes of Finite Structures. | Anuj Dawar, David Richerby |
| 2007 | Model-Checking First-Order Logic: Automata and Locality. | Anuj Dawar |
| 2007 | Subexponential Time and Fixed-Parameter Tractability: Exploiting the Miniaturization Mapping. | Yijia Chen, Jrg Flum |
| 2007 | MSO on the Infinite Binary Tree: Choice and Order. | Arnaud Carayol, Christof Lding |
| 2007 | Unbounded Proof-Length Speed-Up in Deduction Modulo. | Guillaume Burel |