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

https://hal.archives-ouvertes.fr/hal-03123968
Contributeur : Marie Kerjean <>
Soumis le : jeudi 28 janvier 2021 - 12:06:06
Dernière modification le : mercredi 10 février 2021 - 03:20:55

Fichier

main_hal_version.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-03123968, version 1

Citation

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

Partager

Métriques

Consultations de la notice

9

Téléchargements de fichiers

4