Paper Info
Title
A Co-inductive Approach to Real Numbers
Abstract
We define constructive real numbers in the logical framework Coq using streams, i.e. infinite sequences of digits. Co-inductive types and co-inductive proofs permit to work naturally on this representation. We prove our representation satisfies a set of basic properties which we propose as a set of axioms for constructive real numbers.
Year
DOI
Venue
1999
10.1007/3-540-44557-9_7
TYPES
Keywords
Field
DocType
logical framework coq,real numbers,co-inductive approach,basic property,co-inductive type,constructive real number,co-inductive proof,satisfiability,logical framework
Construction of the real numbers,Discrete mathematics,Axiomatic system,Constructive,Computer science,Axiom,Real analysis,Algorithm,Mathematical proof,Real number,Interval (mathematics)
Conference
ISBN
Citations 
PageRank 
3-540-41517-3
9
1.68
References 
Authors
7
2
Name
Order
Citations
PageRank
Alberto Ciaffaglione1589.97
pietro di gianantonio216717.30