A certified, corecursive implementation of exact real numbers

DOI10.1016/J.TCS.2005.09.061MaRDI QIDQ817858zbMATH OpenOpenAlexFDO

Authors Alberto Ciaffaglione, Pietro Di Gianantonio

Publication date 20 March 2006

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2005.09.061

zbMATH Keywords

coinductive type theoriesCoqexact computationinteractive theorem provinglazy functional algorithmslogical frameworksprogram and system verificationstreams of digits

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60)

Recommendations

• scientific article; zbMATH DE number 1696612
• Coinductive field of exact real numbers and general corecursion
• Coinduction for exact real number computation
• From Coinductive Proofs to Exact Real Arithmetic
• Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base

Cites work

• Constructive mathematics: a foundation for computable analysis
• Constructivism in mathematics. An introduction. Volume I
• scientific article; zbMATH DE number 1696612 (Why is no real title available?)
• scientific article; zbMATH DE number 3548474 (Why is no real title available?)
• scientific article; zbMATH DE number 2061716 (Why is no real title available?)
• scientific article; zbMATH DE number 1460545 (Why is no real title available?)
• scientific article; zbMATH DE number 2085165 (Why is no real title available?)
• scientific article; zbMATH DE number 2085168 (Why is no real title available?)
• scientific article; zbMATH DE number 3291139 (Why is no real title available?)
• Implementing constructive real analysis (preliminary report)
• The calculus of constructions

Cited in

(30)

• Coinduction for exact real number computation
• Polynomial time over the reals with parsimony
• Axiomatic reals and certified efficient exact real computation
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
• Soundness and completeness proofs by coinductive methods
• scientific article; zbMATH DE number 1696612 (Why is no real title available?)
• ROSCoq: robots powered by constructive reals
• Formalization of real analysis: a survey of proof assistants and libraries
• Constructive analysis, types and exact real numbers
• Affine functions and series with co-inductive real numbers
• A monadic, functional implementation of real numbers
• Certified Exact Transcendental Real Number Computation in Coq
• Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers
• From Coinductive Proofs to Exact Real Arithmetic
• scientific article; zbMATH DE number 1231646 (Why is no real title available?)
• Type classes for efficient exact real arithmetic in \textsc{Coq}
• Implementing real numbers with RZ
• Logic for exact real arithmetic
• Limits of real numbers in the binary signed digit representation
• Computing with continuous objects: a uniform co-inductive approach
• Computer Certified Efficient Exact Reals in Coq
• Efficient Exact Arithmetic over Constructive Reals
• Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
• Program extraction in exact real arithmetic
• Some representations of real numbers using integer sequences
• Logic for Exact Real Arithmetic: Multiplication
• scientific article; zbMATH DE number 7731929 (Why is no real title available?)
• Computable analysis for verified exact real computation
• Proofs, programs, processes
• The world's shortest correct exact real arithmetic program?

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A certified, corecursive implementation of exact real numbers

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