Skip to main content
PRL Project



next up previous
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.