DIFFERENTIAL CALCULUS
PROGRAMMING LANGUAGES

A Simply Typed λ-Calculus of Forward Automatic Differentiation

Resource type
Author/contributor
Title
A Simply Typed λ-Calculus of Forward Automatic Differentiation
Abstract
We present an extension of the simply typed λ-calculus with pushforward operators. This extension is motivated by the desire to incorporate forward automatic differentiation, which is an important technique in numeric computing, into functional programming. Our calculus is similar to Ehrhard and Regnierʼs differential λ-calculus, but is based on the differential geometric idea of pushforward rather than derivative. We prove that, like the differential λ-calculus, our calculus can be soundly interpreted in differential λ-categories.
Publication
Electronic Notes in Theoretical Computer Science
Volume
286
Pages
257-272
Date
September 24, 2012
Series
Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII)
Journal Abbr
Electronic Notes in Theoretical Computer Science
Language
en
DOI
10/ggdm57
ISSN
1571-0661
Accessed
2019-11-28T18:09:40Z
Library Catalog
ScienceDirect
Extra
ZSCC: 0000013
Citation
Manzyuk, O. (2012). A Simply Typed λ-Calculus of Forward Automatic Differentiation. Electronic Notes in Theoretical Computer Science, 286, 257–272. https://doi.org/10/ggdm57
PROGRAMMING LANGUAGES
Processing time: 0.02 seconds

Graph of references

(from Zotero to Gephi via Zotnet with this script)
Graph of references