Niko Matsakis, one of the core Rust contributors, is going to present some proof techniques from Prolog that are informing some advanced work in Rust's type checker and compiler.
Traditional Prolog lets you define logical relationships and then have the solver figure out the inferences. But Prolog's Horn Clauses are fairly simplistic in terms of what they can express. This paper talks about a few relatively simple techniques that lets us extend to a much richer logic, supporting things like proving that one statement implies another, or proving "for all" predicates. So for example where Prolog could perhaps setup rules to decide when `hungry(joe)` is true or `hungry(nancy)`, this technique describes techniques to prove `hungry(P)` is true for *any* person P.
"A proof procedure for the logic of hereditary Harrop formulas", Gopalan Nadathur, Journal of Automated Reasoning, Feb 1993, 11(1), pp[masked].