Constructive mathematics in theory and programming practice

Philosophia Mathematica 7 (1):65-104 (1999)
  Copy   BIBTEX

Abstract

The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop's constructive mathematics (BISH). it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructive mathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,998

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Analytics

Added to PP
2009-01-28

Downloads
93 (#184,721)

6 months
17 (#148,367)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Intuitionism.Arend Heyting - 1956 - Amsterdam,: North-Holland Pub. Co..
Over de grondslagen der wiskunde..L. E. J. Brouwer - 1907 - Leipzig,: Maas & van Suchtelen.
Varieties of constructive mathematics.D. S. Bridges - 1987 - New York: Cambridge University Press. Edited by Fred Richman.
Intuitionism, an Introduction.A. Heyting - 1958 - Studia Logica 7:277-278.

View all 24 references / Add more references