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. |
tr (dn b T) empty tr (dn b T) (tr (up b a) empty)