Accéder directement au contenu Accéder directement à la navigation
Pré-publication, Document de travail

∂ is for Dialectica: Typing Differentiable Programming

Abstract : Differentiable programming is a recent research area: its objective is to express differentiation as a modular algorithmic transformation on rich programming languages. It is in particular motivated by the various applications of automatic differentiation in machine learning or formal calculus. This work focuses on the typing system used to express differentiation. The first part of this paper is devoted to expressing the Dialectica transformation as a reverse automated differentiation transformation on a higher-order lambda-calculus with positive types. The second part builds on the intuitions provided by Dialectica to provide a lambda-calculus with an internal differentiation operator, with a typing system inspired by Differential Linear Logic, allowing to express backward automatic differentiation as a callby-name strategy and forward automatic differentiation as a call-by-value strategy. The target language of Dialectica is then given a semantics in smooth models of Differential Linear Logic.
Type de document :
Pré-publication, Document de travail
Liste complète des métadonnées
Contributeur : Marie Kerjean <>
Soumis le : jeudi 4 février 2021 - 10:45:42
Dernière modification le : mercredi 10 février 2021 - 03:20:55


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-03123968, version 2



Marie Kerjean, Pierre-Marie Pédrot. ∂ is for Dialectica: Typing Differentiable Programming. 2021. ⟨hal-03123968v2⟩



Consultations de la notice


Téléchargements de fichiers