cognitive psychology. PhD 
logic programming is seriously slept on, esp. for prototyping PLs -- transcribe an on-paper type system and you get type checking for free from backward chaining why write hundreds of lines of ML only to let it rot after publication?
-
yes! here's some code for the simply-typed λ-calculus and its typing relation in λProlog: http://www.lix.polytechnique.fr/~dale/lProlog/proghol/extract.html#htoc101 … http://www.lix.polytechnique.fr/~dale/lProlog/proghol/extract.html#htoc108 … they show how to ask the λProlog REPL whether a term is of a type, synthesize terms of a type and vice versa, etc. (with some caveats)
Turnstile is also pretty cool! Idk if it's implemented as a translation to logic programming, but it seems to fit this concept. https://dl.acm.org/doi/pdf/10.1145/3009837.3009886 …
