A certified, corecursive implementation of exact real numbers
From MaRDI portal
Publication:817858
DOI10.1016/j.tcs.2005.09.061zbMath1086.68117MaRDI QIDQ817858
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
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
Proofs, programs, processes, Coinduction for exact real number computation, From Coinductive Proofs to Exact Real Arithmetic
Uses Software
Cites Work