Affine functions and series with co-inductive real numbers

DOI10.1017/S0960129506005809zbMath1120.68095OpenAlexW2154701013MaRDI QIDQ3431543

Yves Bertot

Publication date: 12 April 2007

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129506005809

zbMATH Keywords

mechanical verificationalgorithms for exact computation on real numbers

Mathematics Subject Classification ID

Related Items (8)

Real Number Calculations and Theorem Proving ⋮ Proofs, programs, processes ⋮ ``Backward coinduction, Nash equilibrium and the rationality of escalation ⋮ Computer Certified Efficient Exact Reals in Coq ⋮ Constructive Mathematics and Functional Programming (Abstract) ⋮ Coinduction for exact real number computation ⋮ From Coinductive Proofs to Exact Real Arithmetic ⋮ Inductive and Coinductive Components of Corecursive Functions in Coq

Uses Software

• Coq
• RealLib
• SLEEF
• HOL Light
• C-CoRN

This page was built for publication: Affine functions and series with co-inductive real numbers