| 2003 | 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings |
| 2003 | A Proof Theory for Generic Judgments: An extended abstract. Dale Miller, Alwen Fernanto Tiu |
| 2003 | A Sound Framework for Untrusted Verification-Condition Generators. George C. Necula, Robert R. Schneck |
| 2003 | About Translations of Classical Logic into Polarized Linear Logic. Olivier Laurent, Laurent Regnier |
| 2003 | Abstract Saturation-Based Inference. Nachum Dershowitz, Claude Kirchner |
| 2003 | Advice about logical AI. John McCarthy |
| 2003 | An NP Decision Procedure for Protocol Insecurity with XOR. Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, Mathieu Turuani |
| 2003 | Convergence Law for Random Graphs with Specified Degree Sequence. James F. Lynch |
| 2003 | Dependent Intersection: A New Way of Defining Records in Type Theory. Alexei Kopylov |
| 2003 | Formal Verification at Intel. John Harrison |
| 2003 | Homomorphism Closed vs. Existential Positive. Tomás Feder, Moshe Y. Vardi |
| 2003 | Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or. Hubert Comon-Lundh, Vitaly Shmatikov |
| 2003 | Labelled Markov Processes: Stronger and Faster Approximations. Vincent Danos, Josée Desharnais |
| 2003 | Logic in Access Control. Martín Abadi |
| 2003 | Logical Definability and Query Languages over Unranked Trees. Leonid Libkin, Frank Neven |
| 2003 | Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems. Nir Piterman, Moshe Y. Vardi |
| 2003 | Model Checking Guarded Protocols. E. Allen Emerson, Vineet Kahlon |
| 2003 | Model checking for probability and time: from theory to practice . Marta Z. Kwiatkowska |
| 2003 | Model-checking Trace Event Structures. P. Madhusudan |
| 2003 | New Directions in Instantiation-Based Theorem Proving. Harald Ganzinger, Konstantin Korovin |
| 2003 | On Automatic Partial Orders. Bakhadyr Khoussainov, Sasha Rubin, Frank Stephan |
| 2003 | On Program Equivalence in Languages with Ground-Type References. Andrzej S. Murawski |
| 2003 | Orienting Equalities with the Knuth-Bendix Order. Konstantin Korovin, Andrei Voronkov |
| 2003 | Polynomial-time Algorithms from Ineffective Proofs. Paulo Oliva |
| 2003 | Proof Nets for Unit-free Multiplicative-Additive Linear Logic (Extended abstract). Dominic J. D. Hughes, Rob J. van Glabbeek |
| 2003 | Query Evaluation on Compressed Trees (Extended Abstract). Markus Frick, Martin Grohe, Christoph Koch |
| 2003 | Reasoning about Hierarchical Storage. Amal J. Ahmed, Limin Jia, David Walker |
| 2003 | Revisiting Digitization, Robustness, and Decidability for Timed Automata. Joël Ouaknine, James Worrell |
| 2003 | Satisfiability in Alternating-time Temporal Logic. Govert van Drimmelen |
| 2003 | Spectra of Monadic Second-Order Formulas with One Unary Function. Yuri Gurevich, Saharon Shelah |
| 2003 | Spectrum Hierarchies and Subdiagonal Functions. Aaron Hunter |
| 2003 | Strong Bisimilarity on Basic Parallel Processes is PSPACE-complete. Petr Jancar |
| 2003 | Structural Subtyping of Non-Recursive Types is Decidable. Viktor Kuncak, Martin C. Rinard |
| 2003 | Successor-Invariance in the Finite. Benjamin Rossman |
| 2003 | System ST \beta-reduction and completeness. Christophe Raffalli |
| 2003 | The Complexity of Resolution Refinements. Josh Buresh-Oppenheim, Toniann Pitassi |
| 2003 | The Planning Spectrum - One, Two, Three, Infinity. Marco Pistore, Moshe Y. Vardi |
| 2003 | Tractable conservative Constraint Satisfaction Problems. Andrei A. Bulatov |
| 2003 | Types and Programming Languages: The Next Generation. Benjamin C. Pierce |
| 2003 | Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions. Erich Grädel, Stephan Kreutzer |