A certified, corecursive implementation of exact real numbers

DOI10.1016/j.tcs.2005.09.061zbMath1086.68117OpenAlexW2132370466MaRDI QIDQ817858

Pietro Di Gianantonio, Alberto Ciaffaglione

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

interactive theorem provinglogical frameworksCoqexact computationcoinductive type theorieslazy functional algorithmsprogram and system verificationstreams of digits

Mathematics Subject Classification ID

Related Items (13)

Soundness and completeness proofs by coinductive methods ⋮ Limits of real numbers in the binary signed digit representation ⋮ Unnamed Item ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ Unnamed Item ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ Computing with continuous objects: a uniform co-inductive approach ⋮ Proofs, programs, processes ⋮ Program extraction in exact real arithmetic ⋮ Polynomial time over the reals with parsimony ⋮ Coinduction for exact real number computation ⋮ From Coinductive Proofs to Exact Real Arithmetic ⋮ Some representations of real numbers using integer sequences

Uses Software

• Coq

Cites Work

• The calculus of constructions
• Constructivism in mathematics. An introduction. Volume I
• Constructive mathematics: a foundation for computable analysis
• Implementing constructive real analysis (preliminary report)
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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