Programming with Higher-Order Logic

by Dale Miller, Gopalan Nadathur

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

Genres: Computer Science

321 pages, Kindle Edition

First published June 11, 2012

Reviews

[Richard Marmorstein · Rating 3 out of 5]

Having real trouble penetrating this so far. I don't think I'm the target audience. The author seems to place a lot of value on giving a precise formal/technical exposition of the logic programming system than he is imparting intuition to a reader (like me) who is newly come to typed logic programming.

There are very few examples and there are long paragraphs of prose that you can't understand what they mean unless you already understand what they mean.

[Mike Harris · Rating 3 out of 5]

Started off well but I found myself not really understanding the material in the last few chapters. I recommend that you read appendix A first if you plan on working through all of the code content, there are a couple of examples that will not work with Teyjus at the top level and reading the appendix will help you spot those and make adjustments to your code. I did learn a lot about how to implement a type system using prolog and search/pattern matching which was really insightful.