Differentiable Programming and Logic – DiPLo

The theoretical study of programming languages is rooted in discrete structures. However, the computation and approximation of continuous objects are two of the main applications of computer science. The DiPLo project aims to bring programming theory closer to applied mathematics. It will rely on new and surprising links between functional analysis and proof theory, thus enriching the Curry-Howard-Lambek correspondence. DiPLo has three goals: first, we will build a functional, typed, higher-order, differentiable programming language expressing various automatic differentiation techniques. Secondly, we will provide a logical account of the computational content of function approximation techniques. Finally, these advances will lead to a computational understanding of differential equations as a defining paradigm in logic.