A certified, corecursive implementation of exact real numbers
From MaRDI portal
Publication:817858
DOI10.1016/j.tcs.2005.09.061zbMath1086.68117MaRDI 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
interactive theorem proving; logical frameworks; Coq; exact computation; coinductive type theories; lazy functional algorithms; program and system verification; streams of digits
03F60: Constructive and recursive analysis
Related Items
Unnamed Item, Computing with continuous objects: a uniform co-inductive approach, Program extraction in exact real arithmetic, Proofs, programs, processes, Coinduction for exact real number computation, Polynomial time over the reals with parsimony, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting), Soundness and completeness proofs by coinductive methods, Formalization of real analysis: a survey of proof assistants and libraries, From Coinductive Proofs to Exact Real Arithmetic
Uses Software
Cites Work