Coinductive Formal Reasoning in Exact Real Arithmetic

DOI10.2168/LMCS-4(3:6)2008MaRDI QIDQ3535611zbMATH OpenFDO

Authors Milad Niqui

Publication date 13 November 2008

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

Full work available at URL https://doi.org/10.2168/LMCS-4(3:6)2008

zbMATH Keywords

correctnessCoq formalizationcoinductive typesfield operationsEdalat-Potts exact real arithmeticlazy algorithms for computing homographic and quadratic transformationsMöbius mapsrepresentation of real numbers by coinductive streams

Mathematics Subject Classification ID

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

Recommendations

• Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers
• Coinductive field of exact real numbers and general corecursion
• From Coinductive Proofs to Exact Real Arithmetic
• Coinduction for exact real number computation
• New Computational Paradigms

Cited in

(21)

• Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers
• Proofs, programs, processes
• New Computational Paradigms
• Coinduction for exact real number computation
• Typed Lambda Calculi and Applications
• Logic for Exact Real Arithmetic: Multiplication
• Circuits as streams in Coq: verification of a sequential multiplier
• Certified Exact Transcendental Real Number Computation in Coq
• Productivity of Edalat-Potts exact arithmetic in constructive type theory
• Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
• Computer Certified Efficient Exact Reals in Coq
• Formal Verification of Exact Computations Using Newton’s Method
• Affine functions and series with co-inductive real numbers
• Lookahead analysis in exact real arithmetic with logical methods
• From Coinductive Proofs to Exact Real Arithmetic
• Logical Approaches to Computational Barriers
• Realisability and adequacy for (co)induction
• scientific article; zbMATH DE number 1696612 (Why is no real title available?)
• Towards a formal proof system for \(\omega\)-rational expressions
• Coinductive field of exact real numbers and general corecursion
• Types for Proofs and Programs

Describes a project that uses

Uses Software

• Isabelle/ZF
• Coq

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

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