This paper titled "Backpropagation in the Simply Typed Lambda-calculus with Linear Negation" describes how to generalize the backpropagation algorithm used for computational graphs (like in PyTorch or TF) to the simply-typed lambda calculus augmented with a notion of linear negation.
By relying on conceptual tools originating from Linear Logic, the authors prove the correctness of the transformation and its time efficiency.