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.


  1. Page 181, line 3, third character: The term (h a) should be (f a).
  2. Page 210: The last reference should be to ``(Nipkow 1993)'' and not ``Nipkow (1993)''.
  3. Page 268, lines 9 and 8 from the bottom: The symbol trp in both these lines should be tr, i.e. these lines should read
          tr (dn b T) empty
          tr (dn b T) (tr (up b a) empty)

Last updated: 18 July 2012.