λProlog: Logic programming in higher-order logic

The linked Stanford Encyclopedia of Philosophy page on Church’s type theory looks really good. I suffer from the problem that I already understand the topic, but it reads like an actually well written introduction to the topic (for the mathematical or logically minded).