  We characterize Weihrauch reducibility in E-PA$^{\omega}$ + QF-AC$^{0,0}$ and
all systems containing it by the provability in a linear variant of the same
calculus using modifications of G\"odel's Dialectica interpretation that
incorporate ideas from linear logic, nonstandard arithmetic, higher-order
computability, and phase semantics.
