A twist to uKanren to support Higher-Order Relational Programming.
- Unification over beta-eta normal forms
- More advanced lambda-Prolog features such as implication and unversal quantification are not supported.
- Higher-order logic programming usually comes with typed terms, which are not supported at the moment
Recnelty, in the miniKanren workshop 2020, λKanren with both implication and forall goals has been published. You might want to check that out.