| 2000 | A Kripkean Semantics for Dynamic Logic Programming. Ján Sefránek |
| 2000 | A New Model Construction for the Polymorphic Lambda Calculus. Dieter Spreen |
| 2000 | A PVS Proof Obligation Generator for Lustre Programs. Cécile Canovas-Dumas, Paul Caspi |
| 2000 | A Tactic Language for the System Coq. David Delahaye |
| 2000 | An Abstract Interpretation Approach to Termination of Logic Programs. Roberta Gori |
| 2000 | An Extensible Proof Text Editor. Thomas Hallgren, Aarne Ranta |
| 2000 | Behavioural Constructor Implementation for Regular Algebras. Slawomir Lasota |
| 2000 | Binding-Time Analysis by Constraint Solving. A Modular and Higher-Order Approach for Mercury. Wim Vanhoof |
| 2000 | Church's Lambda Delta Calculus. Richard Statman |
| 2000 | Compiling and Verifying Security Protocols. Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron |
| 2000 | Efficient Evaluation Methods for Guarded Logics and Datalog LITE. Erich Grädel |
| 2000 | Efficient First Order Functional Program Interpreter with Time Bound Certifications. Jean-Yves Marion, Jean-Yves Moyen |
| 2000 | Efficient Structural Information Analysis for Real CLP Languages. Roberto Bagnara, Patricia M. Hill, Enea Zaffanella |
| 2000 | Encoding Temporal Logics in Executable Z: A Case Study for the ZETA System. Wolfgang Grieskamp, Markus Lepper |
| 2000 | Equational Binary Decision Diagrams. Jan Friso Groote, Jaco van de Pol |
| 2000 | Graph Operations and Monadic Second-Order Logic: A Survey. Bruno Courcelle |
| 2000 | Have Spass with OCC1N Christian G. Fermüller, Georg Moser |
| 2000 | How to Decide Query Containment Under Constraints Using a Description Logic. Ian Horrocks, Ulrike Sattler, Sergio Tessaris, Stephan Tobies |
| 2000 | Logic Programming Approaches for Representing and Solving Constraint Satisfaction Problems: A Comparison. Nikolay Pelov, Emmanuel De Mot, Marc Denecker |
| 2000 | Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings Michel Parigot, Andrei Voronkov |
| 2000 | On the Alternation-Free Horn Mu-calculus. Jean-Marc Talbot |
| 2000 | On the Complexity of Theory Curbing. Thomas Eiter, Georg Gottlob |
| 2000 | Playing Logic Programs with the Alpha-Beta Algorithm. Jean-Vincent Loddo, Roberto Di Cosmo |
| 2000 | Proof Simplification for Model Generation and Its Applications. Miyuki Koshimura, Ryuzo Hasegawa |
| 2000 | Proof-Search in Implicative Linear Logic as a Matching Problem. Philippe de Groote |
| 2000 | Quantified Propositional Gödel Logics. Matthias Baaz, Agata Ciabattoni, Richard Zach |
| 2000 | Querying Inconsistent Databases. Sergio Greco, Ester Zumpano |
| 2000 | Solving Planning Problems by Partial Deduction. Helko Lehmann, Michael Leuschel |
| 2000 | Static Reduction Analysis for Imperative Object Oriented Languages. Gilles Barthe, Bernard P. Serpette |
| 2000 | The Boundary between Decidable and Undecidable Fragments of the Fluent Calculus. Steffen Hölldobler, Dietrich Kuske |
| 2000 | Using an Abstract Representation to Specialize Functional Logic Programs. Elvira Albert, Michael Hanus, Germán Vidal |