References

BB85

Errett Bishop and Douglas Bridges. Constructive Analysis. NY:Springer-Verlag, 1985.

BC85

Joseph L. Bates and Robert L. Constable. Proofs as programs. ACM Trans. Program. Lang. and Syst., 7(1):53--71, 1985.

Bis67

E. Bishop. Foundations of Constructive Analysis. McGraw-Hill, New York, 1967.

Bis70

E. Bishop. Mathematics as a numerical language. In Intuitionism and Proof Theory., pages 53--71. NY:North-Holland, 1970.

Bro23

L.E.J. Brouwer. On the significance of the principle of excluded middle in mathematics. In J. fur die Reine und Angewandte Math, volume 154, pages 1--2, 1923.

CAB86

Robert L. Constable, S. Allen, H. Bromely, W. Cleaveland, and et al. Implementing Mathematics with the Nuprl Development System. NJ:Prentice-Hall, 1986.

CO78

Robert L. Constable and Michael J. O'Donnell. A Programming Logic. Mass:Winthrop, 1978.

Con71

Robert L. Constable. Constructive mathematics and automatic program writers. In Proc. IFP Congr., pages 229--33, Ljubljana, 1971.

deB80

N.G. deBruijn. A survey of the project automath. Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 589--606, 1980.

Dum77

M. Dummet. Elements of Intuitionism, Oxford Logic Series. Claredon Press, Oxford, 1977.

Hey66

A. Heyting. Intuitionism. North-Holland, Amsterdam, 1966.

Kle52

Stephen C. Kleene. Introduction to Metamathematics. Princeton:van Nostrand, 1952.

ML82

P. Martin-Lof. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153--75. Amsterdam:North Holland, 1982.

Tar44

A. Tarski. The semantic conception of truth and the foundations of semantics. Philos. and Phenom. Res., 4:341--376, 1944.

Tro73

A. Troelstra. Metamathematical Investigation of Intuitionistic Mathematics. Springer-Verlag, New York, 1973.