Coinductive field of exact real numbers and general corecursion

MaRDI QIDQ2863898zbMATH OpenFDO

Authors Milad Niqui

Publication date 4 December 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066106004737?np=y

zbMATH Keywords

coinductive typesexact real arithmeticgeneral corecursion

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Computation over the reals, computable analysis (03D78) Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 1696612
• A coinductive approach to real analysis
• From Coinductive Proofs to Exact Real Arithmetic
• From coinductive proofs to exact real arithmetic: theory and applications
• Coinductive Formal Reasoning in Exact Real Arithmetic
• scientific article; zbMATH DE number 2085168
• scientific article; zbMATH DE number 705075
• An Intuitionistic Axiomatisation of Real Closed Fields
• The Degrees of Constructibility of Cohen Reals
• scientific article; zbMATH DE number 3995745

Cited in

(11)

• Coinduction for exact real number computation
• Inductive and coinductive components of corecursive functions in Coq
• The Degrees of Constructibility of Cohen Reals
• Coinductive Formal Reasoning in Exact Real Arithmetic
• Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers
• Using Structural Recursion for Corecursion
• From Coinductive Proofs to Exact Real Arithmetic
• On coalgebra of real numbers
• Infinite powers and Cohen reals
• scientific article; zbMATH DE number 2085168 (Why is no real title available?)
• A certified, corecursive implementation of exact real numbers

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Coinductive field of exact real numbers and general corecursion

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