The book argues for using higher-order intuitionistic logic as the foundations of logic programming. To support this argument, the book presents
The book also emphasizes the practical application of higher-order logic programming by showing that it can be used to provide elegant formalizations and implementations of computations that manipulate bindings in syntax. In addition to a general exposition of this approach, individual chapters present extended examples relating to
The λProlog language is used to illustrated the underlying computation-related ideas and their applications. The website for the book provides all the λProlog code used in the book. The reader can experiment with this code using the Teyjus compiler available from http://teyjus.cs.umn.edu/.