| 2003 | Logical Definability and Query Languages over Unranked Trees. | Leonid Libkin, Frank Neven |
| 2003 | About Translations of Classical Logic into Polarized Linear Logic. | Olivier Laurent, Laurent Regnier |
| 2003 | Model checking for probability and time: from theory to practice . | Marta Z. Kwiatkowska |
| 2003 | Structural Subtyping of Non-Recursive Types is Decidable. | Viktor Kuncak, Martin C. Rinard |
| 2003 | Orienting Equalities with the Knuth-Bendix Order. | Konstantin Korovin, Andrei Voronkov |
| 2003 | Dependent Intersection: A New Way of Defining Records in Type Theory. | Alexei Kopylov |
| 2003 | On Automatic Partial Orders. | Bakhadyr Khoussainov, Sasha Rubin, Frank Stephan |
| 2003 | Strong Bisimilarity on Basic Parallel Processes is PSPACE-complete. | Petr Jancar |
| 2003 | Spectrum Hierarchies and Subdiagonal Functions. | Aaron Hunter |
| 2003 | Proof Nets for Unit-free Multiplicative-Additive Linear Logic (Extended abstract). | Dominic J. D. Hughes, Rob J. van Glabbeek |
| 2003 | Formal Verification at Intel. | John Harrison |
| 2003 | Spectra of Monadic Second-Order Formulas with One Unary Function. | Yuri Gurevich, Saharon Shelah |
| 2003 | Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions. | Erich Grdel, Stephan Kreutzer |
| 2003 | New Directions in Instantiation-Based Theorem Proving. | Harald Ganzinger, Konstantin Korovin |
| 2003 | Query Evaluation on Compressed Trees (Extended Abstract). | Markus Frick, Martin Grohe, Christoph Koch |
| 2003 | Homomorphism Closed vs. Existential Positive. | Toms Feder, Moshe Y. Vardi |
| 2003 | Model Checking Guarded Protocols. | E. Allen Emerson, Vineet Kahlon |
| 2003 | Satisfiability in Alternating-time Temporal Logic. | Govert van Drimmelen |
| 2003 | Abstract Saturation-Based Inference. | Nachum Dershowitz, Claude Kirchner |
| 2003 | Labelled Markov Processes: Stronger and Faster Approximations. | Vincent Danos, Jose Desharnais |
| 2003 | Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or. | Hubert Comon-Lundh, Vitaly Shmatikov |
| 2003 | An NP Decision Procedure for Protocol Insecurity with XOR. | Yannick Chevalier, Ralf Ksters, Michal Rusinowitch, Mathieu Turuani |
| 2003 | The Complexity of Resolution Refinements. | Josh Buresh-Oppenheim, Toniann Pitassi |
| 2003 | Tractable conservative Constraint Satisfaction Problems. | Andrei A. Bulatov |
| 2003 | Reasoning about Hierarchical Storage. | Amal J. Ahmed, Limin Jia, David Walker |