Backpropagation in the Simply Typed Lambda-Calculus With Linear Negation