λProlog: Logic programming in higher-order logic λProlog is a logic programming language based on higher-order intuitionistic logic in the style of Church's Simple Theory of Types. Such a strong logical foundation provides λProlog with logically supported notions of modular programming, abstract datatypes, higher-order programming, and the lambda-tree syntax approach to the treatment of bound vari