Automatic differentiation in ACL2

DOI10.1007/978-3-642-22863-6_23MaRDI QIDQ3088015zbMATH OpenOpenAlexFDO

Authors Peter Reid, Ruben A. Gamboa

Publication date 17 August 2011

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-22863-6_23

zbMATH Keywords

automatic differentiationnonstandard analysisACL2

Mathematics Subject Classification ID

Differentiation (real functions of one variable): general theory, generalized derivatives, mean value theorems (26A24) Nonstandard analysis (26E35) Software, source code, etc. for problems pertaining to real functions (26-04)

Recommendations

• Perspectives on automatic differentiation: fast, present, and future?
• scientific article; zbMATH DE number 992807
• Automatic differentiation and its program realization
• The Arithmetic of Differentiation
• A mathematical view of automatic differentiation

Cites work

• scientific article; zbMATH DE number 1722949 (Why is no real title available?)
• Evaluating Derivatives
• Nonstandard analysis in ACL2
• On formal certification of AD transformations
• On the implementation of automatic differentiation tools

Cited in

(5)

• Implementing an automatic differentiator in ACL2
• Mixed-language automatic differentiation
• A language for differentiable functions
• An ADA library for automatic evaluation of derivatives
• Formalization of real analysis: a survey of proof assistants and libraries

Describes a project that uses

Uses Software

• Autodiff
• ADIC
• ADIFOR
• ACL2

This page was built for publication: Automatic differentiation in ACL2

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3088015)