Miller and Gopalan
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.
- Page 181, line 3, third character: The term (h a) should
be (f a).
- Page 210: The last reference should be to ``(Nipkow 1993)'' and
not ``Nipkow (1993)''.
- 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.