This volume contains the papers presented at the 1999 International C- ference on Principles and Practice of Declarative Programming (PPDP'99) held in Paris from September 29 through October 1, 1999. PPDP'99 participated, together with the International Conference on Functional Programming (ICFP) and several related workshops, in a federation of colloquia known as Principles, Logics and Implementations of high-level programming languages(PLI'99). The overall event was organized by the Institut National de Recherche en Inf- matique et en Automatique (INRIA) and the ACM Special Interest Group for Programming Languages (ACM/SIGPLAN). PPDP represents the union of two conferences that had been in existence for about a decade: Programming Languages, Implementations, Logics and P- grams(PLILP)andAlgebraicandLogicProgramming(ALP). Theseconferences wereheldasoneforthe?rsttimeunderthenamePLILP/ALPintheirtenthand seventhrespectiveincarnationslastyear. Thepresentrenditionfollowsadecision bythe combinedsteering committees to adopta simpler namefor the conference that also re?ected the union. Continuing the tradition of PLILP/ALP, PPDP aims to stimulate research in the use of declarative methods in programming and on the design, application, and implementation of programming languages that support such methods. Topics of interest include the use of type theory, logics, and logical methods in understanding, de?ning, integrating, and exte- ing programming paradigms such as those for functional, logic, object-oriented, constraint, and concurrentprogramming;support for modularity;the use of l- ics in the design of program development tools; development of implementation methods; and the application of the relevant paradigms and associated methods in industry and education. Many of these themes are re?ected in the papers appearing in the present collection.

Formal systems that describe computations over syntactic structures occur frequently in computer science. Logic programming provides a natural framework for encoding and animating such systems. However, these systems often embody variable binding, a notion that must be treated carefully at a computational level. This book aims to show that a programming language based on a simply typed version of higher-order logic provides an elegant, declarative means for providing such a treatment. Three broad topics are covered in pursuit of this goal. First, a proof-theoretic framework that supports a general view of logic programming is identified. Second, an actual language called Prolog is developed by applying this view to higher-order logic. Finally, a methodology for programming with specifications is exposed by showing how several computations over formal objects such as logical formulas, functional programs, and -terms and -calculus expressions can be encoded in Prolog.