Comment by jpt4

The Curry-Howard Correspondence is more of an observation than a theorem, but insofar as it describes the general concept of relating logics and programming languages, what is the CHC for logic programming languages? If strikes me that LP directly instantiates and manipulates logical expressions, in a "self-dual" sense; or, is it that the various "proof procedures" of the logic side map to "proof search" algorithms on the computing side?