Programming with Higher-Order Logic
by and Gopalan Nadathur.
Published by Cambridge University Press, June 2012.

Programming with Higher-order Logic focuses on how logic programming can exploit higher-order intuitionistic logic. The authors emphasize using higher-order logic programming to declaratively specify a range of applications.


Order this book from,, or directly from Cambridge University Press.

Book jacket description

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 and declarative means for realizing 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 a higher-order logic. Finally, a methodology for computing with specifications is exposed by showing how several computations over formal objects such as logical formulas, functional programs, λ-terms, and π-calculus expressions can be encoded in λProlog.

Additional material

  1. The table of contents.
  2. An errata.
  3. All the code fragments contained in the book can be found on this one web page. You can use this page to search for bits of code and then cut-and-paste them into editors in order to experiment with the books example in, say, the Teyjus compiler.

Some Links

  1. λProlog home page
  2. Teyjus implementation of λProlog
  3. Wikipedia entry for λProlog

Last updated: 18 July 2012.