**Next:**About this document

**Up:**Formalizing Constructive Real Analysis

**Previous:**Tactic Code

## References

**1**-
E. Bishop.
*Foundations of Constructive Analysis*. McGraw-Hill, New York, 1967. **2**-
D. S. Bridges.
*Constructive Functional Analysis*. Pitman, London, 1979. **3**-
F. Brown, J. Chirimar and D. J. Howe, unpublished Nuprl libraries.
**4**-
J. Chirimar and D. J. Howe. Implementing Constructive Real Analysis: A
Preliminary Report. In
*Symposium on Constructivity in Computer Science*,*Lecture Notes in Computer Science*, Springer Verlag, 1991. **5**-
R. L. Constable, et al.
*Implementing Mathematics with the Nuprl Proof Development System*. Prentice-Hall, Englewood Cliffs, New Jersey, 1986. **6**-
W. M. Farmer and F. J. Thayer, Two Computer-Supported Proofs in Metric Space
Topology,
*Notices of the AMS*, Nov 1991, Vol. 38, number 9, pp. 1133--1138. **7**-
J. Harrison, Constructing the real numbers in Higher Order Logic.
**8**-
J. Harrison and L. Théry, Extending the HOL theorem prover with a Computer
Algebra System to Reason about the Reals.
**9**- J. T. Udding, A Theory of Real Numbers and its Presentation in AUTOMATH, Vol. I--III, Master's Thesis, Eindhoven University of Technology, 1980.