1: \begin{thebibliography}{10}
2:
3: \bibitem{Coq:2007}
4: The {Coq} {Development}~{Team}.
5: \newblock {\em The {Coq} Reference Manual, version 8.1}, February 2007.
6: \newblock Distributed electronically at \url{http://coq.inria.fr/doc}.
7:
8: \bibitem{cornsrc}
9: {Constructive Coq Repository at Nijmegen}, 2008.
10: \newblock \url{http://corn.cs.ru.nl/}.
11:
12: \bibitem{luisthesis}
13: Lu\'is Cruz-Filipe.
14: \newblock {\em Constructive Real Analysis: a Type-Theoretical Formalization and
15: Applications}.
16: \newblock PhD thesis, University of Nijmegen, April 2004.
17:
18: \bibitem{lcf04-corn}
19: Lu\'{\i}s Cruz-Filipe, Herman Geuvers, and Freek Wiedijk.
20: \newblock {C-CoRN}, the constructive coq repository at nijmegen.
21: \newblock In Andrea Asperti, Grzegorz Bancerek, and Andrzej Trybulec, editors,
22: {\em MKM}, volume 3119 of {\em Lecture Notes in Computer Science}, pages
23: 88--103. Springer, 2004.
24:
25: \bibitem{cornhierarchy}
26: Herman Geuvers, Randy Pollack, Freek Wiedijk, and Jan Zwanenburg.
27: \newblock A constructive algebraic hierarchy in {C}oq.
28: \newblock {\em Journal of Symbolic Computation, Special Issue on the
29: Integration of Automated Reasoning and Computer Algebra Systems},
30: 34(4):271--286, 2002.
31:
32: \bibitem{harrison-thesis}
33: John Harrison.
34: \newblock {\em Theorem Proving with the Real Numbers}.
35: \newblock Springer-Verlag, 1998.
36:
37: \bibitem{lester:2008}
38: David~R. Lester.
39: \newblock Real number calculations and theorem: Proving validation and use of
40: an exact arithmetic.
41: \newblock In Otmane Ait-Mohamed, editor, {\em TPHOLs}, volume 5170 of {\em
42: Lecture Notes in Computer Science}, pages 215--229. Springer, 2008.
43:
44: \bibitem{Letouzey02}
45: Pierre Letouzey.
46: \newblock A new extraction for {C}oq.
47: \newblock In Herman Geuvers and Freek Wiedijk, editors, {\em TYPES}, volume
48: 2646 of {\em Lecture Notes in Computer Science}, pages 200--219. Springer,
49: 2002.
50:
51: \bibitem{Mel08b}
52: Guillaume Melquiond.
53: \newblock Proving bounds on real-valued functions with computations.
54: \newblock In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors,
55: {\em Proceedings of the 4th International Joint Conference on Automated
56: Reasoning}, Lectures Notes in Computer Science, Sydney, Australia, 2008.
57:
58: \bibitem{isabelle}
59: Tobias Nipkow, Lawrence~C. Paulson, and Markus Wenzel.
60: \newblock {\em Isabelle/HOL - A Proof Assistant for Higher-Order Logic}, volume
61: 2283 of {\em Lecture Notes in Computer Science}.
62: \newblock Springer, 2002.
63:
64: \bibitem{miladsthesis}
65: Milad Niqui.
66: \newblock {\em Formalising Exact Arithmetic: Representations, Algorithms and
67: Proofs}.
68: \newblock PhD thesis, Radboud Universiteit Nijmegen, September 2004.
69:
70: \bibitem{obuaphd}
71: Steven Obua.
72: \newblock {\em Flyspeck II: The Basic Linear Programs}.
73: \newblock PhD thesis, Technische Universitat Munchen, 2008.
74: \newblock submitted.
75:
76: \end{thebibliography}
77: