Automatic differentiation in ACL2

DOI10.1007/978-3-642-22863-6_23zbMATH Open1342.68301OpenAlexW2280334138MaRDI QIDQ3088015FDOQ3088015

Ruben A. Gamboa, Peter Reid

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

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

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)

Cites Work

• Evaluating Derivatives
• Nonstandard analysis in ACL2
• Title not available (Why is that?)
• On the implementation of automatic differentiation tools
• On formal certification of AD transformations

Cited In (4)

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

Uses Software

• ACL2
• ADIFOR
• ADIC
• Autodiff

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)