[Agda] Book Announcement

[Gopalan Nadathur]

Dale Miller and I are happy to announce the recent publication of our
book entitled "Programming with Higher-Order Logic" by Cambridge
University Press. The table of contents and other details about the
book can be found at https://sites.google.com/site/proghol/.

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 system available from
http://teyjus.cs.umn.edu/.