A tour with constructive real numbers

DOI10.1007/3-540-45842-5_3MaRDI QIDQ4736388zbMATH OpenFDO

Authors Alberto Ciaffaglione, Pietro Di Gianantonio

Publication date 9 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2277/22770041.htm

zbMATH Keywords

constructive real numbersminimal axiomatization

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Constructive and recursive analysis (03F60)

Recommendations

• A natural construction for the real numbers
• Generalized real numbers in constructive mathematics
• Two concrete new constructions of the real numbers
• On the constructive Dedekind reals
• scientific article; zbMATH DE number 4012709
• scientific article; zbMATH DE number 5071262
• Real analysis. A constructive approach
• Real analysis. A constructive approach

Cited in

(2)

• Constructing the real numbers in HOL
• A certified, corecursive implementation of exact real numbers

This page was built for publication: A tour with constructive real numbers

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