Residual Theory in λ-Calculus: A Formal Development