scientific article; zbMATH DE number 2085168

zbMath1054.03039MaRDI QIDQ4736391

Milad Niqui, Herman Geuvers

Publication date: 9 August 2004

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

Coq proof assistantconstructive real numbers

Mathematics Subject Classification ID

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

Related Items

Wave equation numerical resolution: a comprehensive mechanized proof of a C program, Proofs of randomized algorithms in Coq, Certified Exact Transcendental Real Number Computation in Coq, An induction principle over real numbers, Coquelicot: a user-friendly library of real analysis for Coq, Unnamed Item, A certified, corecursive implementation of exact real numbers

Uses Software

• Coq