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.