How Incomputable is the Separable Hahn-Banach Theorem?

We investigate some basic connections between reverse mathematics and computable analysis. In particular, we show how to use Weak König's Lemma within the framework of computable analysis to classify incomputable functions of low complexity. By defining the multi-valued function Sep and through the definition of a natural notion of reducibility for multi-valued functions, we obtain a computational counterpart of the subsystem of second order arithmetic WKL0. We study analogies and differences between WKL0 and the class of Sep-computable multi-valued functions. We use these notions to provide a method to determine the computational complexity of the Hahn-Banach Extension Theorem.