Programming with higher-order logic. (Q2891520)

Dale Miller, a recipient of the prestigious Advanced ERC Grant, wrote together with Gopalan Nadathur this book on programming with higher-order logic, and \(\lambda\)Prolog in particular. The result is a book that seems most suited for those that have a strong background in logic and less so for programmers of higher-order functional languages such as Haskell and ML. Although the logics are illustrated by many examples, the book is more foundational than a programming language reference. Indeed, quite a few of these examples serve to illustrate a particular point to be made about the logic(s), and not so much explain how to design a solution to a problem in the language.NEWLINENEWLINEThe motivation for looking at higher-order logic languages, and \(\lambda\)Prolog in particular, is that it allows for the definition of the syntax of programming languages and declaratively specifying the static and dynamic semantics of such complex languages, in particular when it comes to the notion of binding in these languages (case studies include the implementation of proof systems, a small functional language, and the \(\pi\)-calculus). The case studies are provided at the very end of the book, and one wonders whether these could have obtained a more central place, as the proverbial carrot for making the reader want to know exactly how this is done. As it is, the reader has to go through a substantial amount of logic (languages) before getting to his or her reward. Having to go through a series of logics is not a bad thing in itself because it does allow the authors to gradually build from first-order terms and Horn clauses towards higher-order logic.NEWLINENEWLINEThe book is written in an immaculate, authorative style, mistakes are very few, and no word is wasted. Not much of a logic programmer myself, the bibliographic notes that (also) relate the material to the world outside logic programming were enlightening. Often it turned out that I had to drop some of my preconceptions about the nature of programming (that I have gleaned from a functional language), in order to fully appreciate this book. It is clear that some pretty cool things can be done in \(\lambda\)Prolog, and in an extremely declarative way at that.