Programming with Higher-Order Logic

Programming with Higher-Order Logic
Dale Miller and Gopalan Nadathur
Cambridge University Press 2013

Church's higher-order logic, based on the typed $\lambda$-calculus, is a foundation of mathematics and computer science.  It underpins a number of other influential logics and type theories, including systems for formalized mathematics such as LF, HOL and Coq, which in turn have led to interesting developments relevant to mainstream mathematics such as formal proofs of the Four-Color Theorem and Feit-Thompson Theorem in Coq, as well as the Homotopy Type Theory program initiated by Voevodsky.  This book is about higher-order logic viewed in a different light, as a foundation for programming, specifically following the computation-as-deduction approach taken in logic programming languages such as Prolog.  Higher-order logic programming builds on higher-order unification, and generalizes Horn clauses over first-order terms in Prolog to hereditary Harrop formulas over higher-order terms in languages such as $\lambda$Prolog. One might view (higher-order) logic programming as a tool deserving a place in a logician's toolbox analogous to numerical or symbolic tools for analysis: not a replacement for mathematical reasoning, but a framework for experimentation and automation.

Read more »