A monadic, functional implementation of real numbers

DOI10.1017/S0960129506005871MaRDI QIDQ3431547zbMATH OpenFDO

Authors Russell O'Connor

Publication date 12 April 2007

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0960129506005871

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Constructive and recursive analysis (03F60) Functional programming and lambda calculus (68N18)

Recommendations

• A computer-verified monadic functional implementation of the integral
• scientific article; zbMATH DE number 1222580
• The constructive reals as a Java library
• Certified Exact Transcendental Real Number Computation in Coq
• A certified, corecursive implementation of exact real numbers

Cited in

(13)

• The constructive reals as a Java library
• Coquelicot: a user-friendly library of real analysis for Coq
• Formalization of real analysis: a survey of proof assistants and libraries
• A formal study of Bernstein coefficients and polynomials
• Certified Exact Transcendental Real Number Computation in Coq
• Implementing real numbers with RZ
• Computer Certified Efficient Exact Reals in Coq
• Constructive Mathematics and Functional Programming (Abstract)
• Topological quantum gates in homotopy type theory
• Extracting efficient exact real number computation from proofs in constructive type theory
• Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis
• The interval domain in homotopy type theory
• A computer-verified monadic functional implementation of the integral

Describes a project that uses

Uses Software

• Haskell

This page was built for publication: A monadic, functional implementation of real numbers

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