| 2000 | A Tactic Language for the System Coq. | David Delahaye |
| 2000 | Graph Operations and Monadic Second-Order Logic: A Survey. | Bruno Courcelle |
| 2000 | A PVS Proof Obligation Generator for Lustre Programs. | Ccile Canovas-Dumas, Paul Caspi |
| 2000 | Static Reduction Analysis for Imperative Object Oriented Languages. | Gilles Barthe, Bernard P. Serpette |
| 2000 | Efficient Structural Information Analysis for Real CLP Languages. | Roberto Bagnara, Patricia M. Hill, Enea Zaffanella |
| 2000 | Quantified Propositional Gdel Logics. | Matthias Baaz, Agata Ciabattoni, Richard Zach |
| 2000 | Using an Abstract Representation to Specialize Functional Logic Programs. | Elvira Albert, Michael Hanus, Germn Vidal |
| 1999 | Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups. | Uwe Waldmann |
| 1999 | Regular Sets of Descendants for Constructor-Based Rewrite Systems. | Pierre Rty |
| 1999 | Proving Failure of Queries for Definite Logic Programs Using XSB-Prolog. | Nikolay Pelov, Maurice Bruynooghe |
| 1999 | Transforming Conditional Rewrite Systems with Extra Variables into Unconditional Systems. | Enno Ohlebusch |
| 1999 | Abstracting Properties in Concurrent Constraint Programming. | Ren Moreno |
| 1999 | Animating TLA Specifications. | Yassin Mokhtari, Stephan Merz |
| 1999 | Complexity of Terminological Reasoning Revisited. | Carsten Lutz |
| 1999 | Resource Management in Linear Logic Search Revisited. | Pablo Lpez, Ernesto Pimentel |
| 1999 | Model Checking Games for the Alternation-Free µ-Calculus and Alternating Automata. | Martin Leucker |
| 1999 | Practical Reasoning for Expressive Description Logics. | Ian Horrocks, Ulrike Sattler, Stephan Tobies |
| 1999 | Beth Definability for the Guarded Fragment. | Eva Hoogland, Maarten Marx, Martin Otto |
| 1999 | On the Complexity of Counting the Hilbert Basis of a Linear Diophnatine System. | Miki Hermann, Laurent Juban, Phokion G. Kolaitis |
| 1999 | Extensions to the Estimation Calculus. | Jeremy Gow, Alan Bundy, Ian Green |
| 1999 | On the Complexity of Single-Rule Datalog Queries. | Georg Gottlob, Christos H. Papadimitriou |
| 1999 | A Fixpoint Semantics for Reasoning about Finite Failure. | Roberta Gori |
| 1999 | Simplification of Horn Clauses That Are Clausal Forms of Guarded Formulas. | Michael Dierkes |
| 1999 | CHAT Is Theta(SLG-Wam). | Bart Demoen, Konstantinos Sagonas |
| 1999 | Evidence Algorithm and Sequent Logical Inference Search. | Anatoli Degtyarev, Alexander V. Lyaletski, Marina K. Morokhovets |