Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base

DOI10.1007/978-3-540-78969-7_6MaRDI QIDQ5458427zbMATH OpenOpenAlexFDO

Authors Nicolas Julien

Publication date 11 April 2008

Published in Functional and Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78969-7_6

Mathematics Subject Classification ID

Recommendations

• A certified, corecursive implementation of exact real numbers
• Certified Exact Transcendental Real Number Computation in Coq
• Coinduction for exact real number computation
• From Coinductive Proofs to Exact Real Arithmetic
• Axiomatic reals and certified efficient exact real computation
• From coinductive proofs to exact real arithmetic: theory and applications
• Computer Certified Efficient Exact Reals in Coq
• Coinductive Formal Reasoning in Exact Real Arithmetic
• Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers
• Efficient Exact Arithmetic over Constructive Reals

Cited in

(10)

• Type classes for efficient exact real arithmetic in \textsc{Coq}
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• A certified, corecursive implementation of exact real numbers
• Efficient Exact Arithmetic over Constructive Reals
• ``Backward coinduction, Nash equilibrium and the rationality of escalation
• Real Number Calculations and Theorem Proving
• Certified Exact Transcendental Real Number Computation in Coq
• Computer Certified Efficient Exact Reals in Coq
• Formal Verification of Exact Computations Using Newton’s Method
• From Coinductive Proofs to Exact Real Arithmetic

Describes a project that uses

Uses Software

• SLEEF
• Coq

This page was built for publication: Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base

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