Next: About this document Up: Formalizing Constructive Real Analysis Previous: Tactic Code
E. Bishop. Foundations of Constructive Analysis.
McGraw-Hill, New York, 1967.
D. S. Bridges. Constructive Functional Analysis.
Pitman, London, 1979.
F. Brown, J. Chirimar and D. J. Howe, unpublished Nuprl libraries.
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.
R. L. Constable, et al. Implementing Mathematics with the Nuprl Proof
Prentice-Hall, Englewood Cliffs, New Jersey, 1986.
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.
J. Harrison, Constructing the real numbers in Higher Order Logic.
J. Harrison and L. Théry, Extending the HOL theorem prover with a Computer
Algebra System to Reason about the Reals.
- J. T. Udding, A Theory of Real Numbers and its Presentation in AUTOMATH, Vol. I--III, Master's Thesis, Eindhoven University of Technology, 1980.