Implementing Real Numbers With RZ

DOI10.1016/j.entcs.2008.03.027zbMath1262.03076OpenAlexW2119156095WikidataQ115902565 ScholiaQ115902565MaRDI QIDQ4918049

Andrej Bauer, Iztok Kavkler

Publication date: 3 May 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.03.027

zbMATH Keywords

realizabilityreal numbersexact real arithmetic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computation over the reals, computable analysis (03D78)

Related Items

The world's shortest correct exact real arithmetic program? ⋮ A constructive theory of continuous domains suitable for implementation ⋮ The Dedekind reals in abstract Stone duality

Uses Software

• RealLib
• MPFR
• OCaml
• iRRAM
• RZ

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Constructivism in mathematics. An introduction. Volume II
• RealLib: An efficient implementation of exact real arithmetic
• Recursive Unsolvability of a problem of Thue
• RZ: A Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item