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

ACL2automatic differentiationnonstandard analysis

Mathematics Subject Classification ID

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

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

• Automatic differentiation of algorithms. From simulation to optimization. Selected papers from the 3rd international conference, Nice, France, June 2000. Incl. 1 CD-ROM
• Evaluating Derivatives
• Nonstandard analysis in ACL2
• On formal certification of AD transformations
• On the implementation of automatic differentiation tools

Cited in

(5)

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

Describes a project that uses

Uses Software

• ACL2
• ADIC
• Autodiff
• ADIFOR

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)