Programmation Differentiable et Logique – DiPLo

L'étude théorique des langages de programmation est ancrée dans celle des structures discrètes. Pourtant, le calcul et l'approximation d'objets continus est l'une des principales applications de l'informatique. Le projet DiPLo vise à rapprocher la théorie de la programmation aux mathématiques appliquées, via la logique. Il le fera en s'appuyant sur des liens nouveaux et surprenants entre l'analyse fonctionnelle et la théorie de la preuve, enrichissant ainsi la correspondance Curry-Howard-Lambek. DiPLo a trois objectifs : tout d'abord, nous construirons un langage de programmation différentiable fonctionnel, typé et d'ordre supérieur exprimant différentes techniques de différentiation automatique. Ensuite, nous rendrons compte en logique du contenu calculatoires des techniques d'approximations de fonctions. Enfin, ces avancées conduiront à une compréhension calculatoire des équations différentielles comme outil logique.