SWIProlog[1] has so far been my go to due to the extensive support system it has. However, I've been meaning to explore higher order logic a bit and Ciao[2] caught my attention there, with sugar for function-like notation and higher order programming including "lambda" style predicate expressions .... and it compiles down to executable. The function notation in this context is along the same lines as Mozart/Oz and can be convenient. Not explore the higher order aspects much though.

[1]: https://www.swi-prolog.org/

[2]: https://en.wikipedia.org/wiki/Ciao_(programming_language)

You won't find much on MIL as "higher-order logic programming" but that's really what it is: it's logic programming; with a higher-order program (i.e. one containing both first- and second-order clauses). The catch is that once you do this any proof you complete gives you instantiations into the second-order variables in the second-order clauses and now you have yourself a first-order program, that you didn't have before; hence "inductive". So it's basically a form of machine learning of logic programs, from other logic programs.

There are a few papers you can find online about MIL, but I recommend (PLUG ALERT) the documentation of the MIL system I created for my doctoral thesis as a starting point:

https://github.com/stassa/louise

I recommend that as a starting point because it's written for people who are familiar with logic programming, but not necessarily ILP. Anyway, plug over. I think MIL is an exciting new development that has of course gone under the radar of the logic programming community at large.