PROGRAMMING WITH HIGHER-ORDER LOGIC
by Dale Miller (INRIA & LIX/Ecole Polytechnique) and
Gopalan Nadathur (University of Minnesota)
Cambridge University Press, ISBN: 9780521879408, 320 pages
http://www.cambridge.org/fr/knowledge/isbn/item6687740
The book argues for using higher-order intuitionistic logic as the foundations of logic programming. In elaborating this argument, the book presents a sequent calculus based characterization of logic programming; a proof search approach to computation; higher-order logic programming; polymorphic typing; modular programming and abstract data types; and simply-typed lambda-terms and their unification.
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 implementing proof systems, computing with functional programs, and encoding the pi-calculus.
The lambda Prolog language is used to illustrate the underlying computation-related ideas and their applications. The website for the book provides all the lambda Prolog code used in the book. The reader can experiment with this code using the Teyjus compiler available from http://teyjus.cs.umn.edu/.
Additional information appears at https://sites.google.com/site/proghol/.