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

exact real arithmeticcoinductive typesgeneral corecursion

Mathematics Subject Classification ID

Computation over the reals, computable analysis (03D78) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) 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)

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

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)