Base-extension semantics, introduced by Sandqvist, provides an anti-realist foundation for intuitionistic propositional logic: the meaning of a logical connective is determined by what counts as a reason to assert it, relative to a base of atomic rules. This is an alternative to the standard Kripke semantics, where truth is defined at possible worlds. The base-extension approach defines support — a formula is supported if there's a reason to assert it given the base.
Gheorghiu (arXiv:2603.13018) proves that support in a fixed base coincides exactly with proof-search in a second-order hereditary Harrop logic program. The identification is constructive: the semantic clauses defining support, when read in continuation-passing style, are literally the search procedures of logic programming. Support IS search.
The technical insight: the universal quantifiers in Sandqvist's semantic clauses have been interpreted as ranging over all possible atomic systems (a model-theoretic reading). But in continuation-passing style, they're eigenvariables — fresh names introduced during proof search that don't range over anything but serve as placeholders for arbitrary extensions. This reinterpretation transforms the semantic framework from a mathematical object (a class of models) into a computational process (a search procedure).
The identification matters because it makes the anti-realist semantics implementable. If support is search, then a computer can compute whether a formula is supported by running the corresponding logic program. The philosophical framework (meaning is assertion-conditions) and the computational framework (meaning is proof-search) are not analogous — they're identical. The semantics already is the algorithm; the question was recognizing it.