Coinductive Formal Reasoning in Exact Real Arithmetic

DOI10.2168/LMCS-4(3:6)2008zbMath1147.68023MaRDI QIDQ3535611

Milad Niqui

Publication date: 13 November 2008

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

zbMATH Keywords

correctnessMöbius mapsCoq formalizationcoinductive typesfield operationsEdalat-Potts exact real arithmeticlazy algorithms for computing homographic and quadratic transformationsrepresentation of real numbers by coinductive streams

Mathematics Subject Classification ID

Analysis of algorithms (68W40) Symbolic computation and algebraic computation (68W30) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Logic in computer science (03B70)

Related Items (3)

Formal Verification of Exact Computations Using Newton’s Method ⋮ Proofs, programs, processes ⋮ From Coinductive Proofs to Exact Real Arithmetic

Uses Software

• Unnamed Item
• Isabelle/ZF

This page was built for publication: Coinductive Formal Reasoning in Exact Real Arithmetic